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 α) :
s.sym2.val = s.val.sym2
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
  • s.sym2 = { val := s.val.sym2, nodup := }
Instances For
    theorem Finset.mk_mem_sym2_iff {α : Type u_1} {s : Finset α} {a : α} {b : α} :
    s(a, b) s.sym2 a s b s
    @[simp]
    theorem Finset.mem_sym2_iff {α : Type u_1} {s : Finset α} {m : Sym2 α} :
    m s.sym2 am, a s
    theorem Finset.sym2_cons {α : Type u_1} (a : α) (s : Finset α) (ha : as) :
    (Finset.cons a s ha).sym2 = (Finset.map (Sym2.mkEmbedding a) (Finset.cons a s ha)).disjUnion s.sym2
    theorem Finset.sym2_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
    (insert a s).sym2 = Finset.image (fun (b : α) => s(a, b)) (insert a s) s.sym2
    theorem Finset.sym2_map {α : Type u_1} {β : Type u_2} (f : α β) (s : Finset α) :
    (Finset.map f s).sym2 = Finset.map f.sym2Map s.sym2
    theorem Finset.sym2_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αβ) (s : Finset α) :
    (Finset.image f s).sym2 = Finset.image (Sym2.map f) s.sym2
    instance Sym2.instFintype {α : Type u_1} [Fintype α] :
    Equations
    • Sym2.instFintype = { elems := Finset.univ.sym2, complete := }
    @[simp]
    theorem Finset.sym2_univ {α : Type u_1} [Fintype α] (inst : optParam (Fintype (Sym2 α)) Sym2.instFintype) :
    Finset.univ.sym2 = Finset.univ
    @[simp]
    theorem Finset.sym2_mono {α : Type u_1} {s : Finset α} {t : Finset α} (h : s t) :
    s.sym2 t.sym2
    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
    theorem Finset.sym2_toFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) :
    m.toFinset.sym2 = m.sym2.toFinset
    @[simp]
    theorem Finset.sym2_empty {α : Type u_1} :
    .sym2 =
    @[simp]
    theorem Finset.sym2_eq_empty {α : Type u_1} {s : Finset α} :
    s.sym2 = s =
    @[simp]
    theorem Finset.sym2_nonempty {α : Type u_1} {s : Finset α} :
    s.sym2.Nonempty s.Nonempty
    theorem Finset.Nonempty.sym2 {α : Type u_1} {s : Finset α} :
    s.Nonemptys.sym2.Nonempty

    Alias of the reverse direction of Finset.sym2_nonempty.

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

    Finset stars and bars for the case n = 2.

    theorem Finset.sym2_eq_image {α : Type u_1} [DecidableEq α] {s : Finset α} :
    s.sym2 = Finset.image Sym2.mk (s ×ˢ s)
    theorem Finset.isDiag_mk_of_mem_diag {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α × α} (h : a s.diag) :
    (Sym2.mk a).IsDiag
    theorem Finset.not_isDiag_mk_of_mem_offDiag {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α × α} (h : a s.offDiag) :
    ¬(Sym2.mk a).IsDiag
    @[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 : α} :
    Sym2.diag a s.sym2 a s
    theorem Finset.image_diag_union_image_offDiag {α : Type u_1} [DecidableEq α] {s : Finset α} :
    Finset.image Sym2.mk s.diag Finset.image Sym2.mk s.offDiag = s.sym2
    instance Finset.instDecidableEqSym {α : Type u_1} [DecidableEq α] {n : } :
    Equations
    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 α} :
      s.sym 0 = {}
      @[simp]
      theorem Finset.sym_succ {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } :
      s.sym (n + 1) = s.sup fun (a : α) => Finset.image (Sym.cons a) (s.sym n)
      @[simp]
      theorem Finset.mem_sym_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } {m : Sym α n} :
      m s.sym n am, a s
      @[simp]
      theorem Finset.sym_empty {α : Type u_1} [DecidableEq α] (n : ) :
      .sym (n + 1) =
      theorem Finset.replicate_mem_sym {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a s) (n : ) :
      Sym.replicate n a s.sym n
      theorem Finset.Nonempty.sym {α : Type u_1} [DecidableEq α] {s : Finset α} (h : s.Nonempty) (n : ) :
      (s.sym n).Nonempty
      @[simp]
      theorem Finset.sym_singleton {α : Type u_1} [DecidableEq α] (a : α) (n : ) :
      {a}.sym n = {Sym.replicate n a}
      theorem Finset.eq_empty_of_sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } (h : s.sym n = ) :
      s =
      @[simp]
      theorem Finset.sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } :
      s.sym n = n 0 s =
      @[simp]
      theorem Finset.sym_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } :
      (s.sym n).Nonempty n = 0 s.Nonempty
      @[simp]
      theorem Finset.sym_univ {α : Type u_1} [DecidableEq α] [Fintype α] (n : ) :
      Finset.univ.sym n = Finset.univ
      @[simp]
      theorem Finset.sym_mono {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) (n : ) :
      s.sym n t.sym n
      @[simp]
      theorem Finset.sym_inter {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (n : ) :
      (s t).sym n = s.sym n t.sym n
      @[simp]
      theorem Finset.sym_union {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) (n : ) :
      s.sym n t.sym n (s t).sym n
      theorem Finset.sym_fill_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } (a : α) {i : Fin (n + 1)} {m : Sym α (n - i)} (h : m s.sym (n - i)) :
      Sym.fill a i m (insert a s).sym n
      theorem Finset.sym_filterNe_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {n : } {m : Sym α n} (a : α) (h : m s.sym n) :
      (Sym.filterNe a m).snd (s.erase a).sym (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 s.sym (n - i) }) :
      ((Finset.symInsertEquiv h).symm m) = Sym.fill a m.fst m.snd
      @[simp]
      theorem Finset.symInsertEquiv_apply_fst {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : } (h : as) (m : { x : Sym α n // x (insert a s).sym n }) :
      ((Finset.symInsertEquiv h) m).fst = (Sym.filterNe a m).fst
      @[simp]
      theorem Finset.symInsertEquiv_apply_snd_coe {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : } (h : as) (m : { x : Sym α n // x (insert a s).sym n }) :
      ((Finset.symInsertEquiv h) m).snd = (Sym.filterNe a m).snd
      def Finset.symInsertEquiv {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : } (h : as) :
      { x : Sym α n // x (insert a s).sym n } (i : Fin (n + 1)) × { x : Sym α (n - i) // x s.sym (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