Documentation

Mathlib.Data.Finset.Sym

Symmetric powers of a finset #

This file defines the symmetric powers of a finset as Finset (Sym α n) and Finset (Sym2 α).

Main declarations #

TODO #

Finset.sym forms a Galois connection between Finset α and Finset (Sym α n). Similar for Finset.sym2.

@[simp]
theorem Finset.sym2_val {α : Type u_1} (s : Finset α) :
def Finset.sym2 {α : Type u_1} (s : Finset α) :

s.sym2 is the finset of all unordered pairs of elements from s. It is the image of s ×ˢ s under the quotient α × α → Sym2 α.

Equations
Instances For
    theorem Finset.mk_mem_sym2_iff {α : Type u_1} {s : Finset α} {a : α} {b : α} :
    s(a, b) Finset.sym2 s a s b s
    @[simp]
    theorem Finset.mem_sym2_iff {α : Type u_1} {s : Finset α} {m : Sym2 α} :
    m Finset.sym2 s am, a s
    instance Sym2.instFintype {α : Type u_1} [Fintype α] :
    Equations
    • Sym2.instFintype = { elems := Finset.sym2 Finset.univ, complete := }
    @[simp]
    theorem Finset.sym2_univ {α : Type u_1} [Fintype α] (inst : optParam (Fintype (Sym2 α)) Sym2.instFintype) :
    Finset.sym2 Finset.univ = Finset.univ
    @[simp]
    theorem Finset.sym2_mono {α : Type u_1} {s : Finset α} {t : Finset α} (h : s t) :
    theorem Finset.monotone_sym2 {α : Type u_1} :
    Monotone Finset.sym2
    theorem Finset.injective_sym2 {α : Type u_1} :
    Function.Injective Finset.sym2
    theorem Finset.strictMono_sym2 {α : Type u_1} :
    StrictMono Finset.sym2
    @[simp]
    @[simp]
    theorem Finset.sym2_eq_empty {α : Type u_1} {s : Finset α} :
    @[simp]
    theorem Finset.sym2_nonempty {α : Type u_1} {s : Finset α} :
    (Finset.sym2 s).Nonempty s.Nonempty
    theorem Finset.Nonempty.sym2 {α : Type u_1} {s : Finset α} :
    s.Nonempty(Finset.sym2 s).Nonempty

    Alias of the reverse direction of Finset.sym2_nonempty.

    @[simp]
    theorem Finset.sym2_singleton {α : Type u_1} (a : α) :
    theorem Finset.card_sym2 {α : Type u_1} (s : Finset α) :
    (Finset.sym2 s).card = Nat.choose (s.card + 1) 2

    Finset stars and bars for the case n = 2.

    theorem Finset.sym2_eq_image {α : Type u_1} [DecidableEq α] {s : Finset α} :
    Finset.sym2 s = Finset.image Sym2.mk (s ×ˢ s)
    theorem Finset.isDiag_mk_of_mem_diag {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α × α} (h : a Finset.diag s) :
    theorem Finset.not_isDiag_mk_of_mem_offDiag {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α × α} (h : a Finset.offDiag s) :
    @[simp]
    theorem Finset.diag_mem_sym2_mem_iff {α : Type u_1} {s : Finset α} {a : α} :
    (bSym2.diag a, b s) a s
    theorem Finset.diag_mem_sym2_iff {α : Type u_1} {s : Finset α} {a : α} :
    instance Finset.instDecidableEqSym {α : Type u_1} [DecidableEq α] {n : } :
    Equations
    • Finset.instDecidableEqSym = Subtype.instDecidableEqSubtype
    def Finset.sym {α : Type u_1} [DecidableEq α] (s : Finset α) (n : ) :
    Finset (Sym α n)

    Lifts a finset to Sym α n. s.sym n is the finset of all unordered tuples of cardinality n with elements in s.

    Equations
    Instances For
      @[simp]
      theorem Finset.sym_zero {α : Type u_1} [DecidableEq α] {s : Finset α} :
      @[simp]
      theorem Finset.sym_succ {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } :
      Finset.sym s (n + 1) = Finset.sup s fun (a : α) => Finset.image (Sym.cons a) (Finset.sym s n)
      @[simp]
      theorem Finset.mem_sym_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } {m : Sym α n} :
      m Finset.sym s n am, a s
      @[simp]
      theorem Finset.sym_empty {α : Type u_1} [DecidableEq α] (n : ) :
      theorem Finset.replicate_mem_sym {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a s) (n : ) :
      theorem Finset.Nonempty.sym {α : Type u_1} [DecidableEq α] {s : Finset α} (h : s.Nonempty) (n : ) :
      (Finset.sym s n).Nonempty
      @[simp]
      theorem Finset.sym_singleton {α : Type u_1} [DecidableEq α] (a : α) (n : ) :
      theorem Finset.eq_empty_of_sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } (h : Finset.sym s n = ) :
      s =
      @[simp]
      theorem Finset.sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } :
      @[simp]
      theorem Finset.sym_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } :
      (Finset.sym s n).Nonempty n = 0 s.Nonempty
      @[simp]
      theorem Finset.sym_univ {α : Type u_1} [DecidableEq α] [Fintype α] (n : ) :
      Finset.sym Finset.univ n = Finset.univ
      @[simp]
      theorem Finset.sym_mono {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) (n : ) :
      @[simp]
      theorem Finset.sym_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (n : ) :
      @[simp]
      theorem Finset.sym_union {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (n : ) :
      theorem Finset.sym_fill_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } (a : α) {i : Fin (n + 1)} {m : Sym α (n - i)} (h : m Finset.sym s (n - i)) :
      theorem Finset.sym_filterNe_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } {m : Sym α n} (a : α) (h : m Finset.sym s n) :
      (Sym.filterNe a m).snd Finset.sym (Finset.erase s a) (n - (Sym.filterNe a m).fst)
      @[simp]
      theorem Finset.symInsertEquiv_symm_apply_coe {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : } (h : as) (m : (i : Fin (n + 1)) × { x : Sym α (n - i) // x Finset.sym s (n - i) }) :
      ((Finset.symInsertEquiv h).symm m) = Sym.fill a m.fst m.snd
      @[simp]
      theorem Finset.symInsertEquiv_apply_snd_coe {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : } (h : as) (m : { x : Sym α n // x Finset.sym (insert a s) n }) :
      ((Finset.symInsertEquiv h) m).snd = (Sym.filterNe a m).snd
      @[simp]
      theorem Finset.symInsertEquiv_apply_fst {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : } (h : as) (m : { x : Sym α n // x Finset.sym (insert a s) n }) :
      ((Finset.symInsertEquiv h) m).fst = (Sym.filterNe a m).fst
      def Finset.symInsertEquiv {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : } (h : as) :
      { x : Sym α n // x Finset.sym (insert a s) n } (i : Fin (n + 1)) × { x : Sym α (n - i) // x Finset.sym s (n - i) }

      If a does not belong to the finset s, then the nth symmetric power of {a} ∪ s is in 1-1 correspondence with the disjoint union of the n - ith symmetric powers of s, for 0 ≤ i ≤ n.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For