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 := }
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} {s : Finset α} [DecidableEq α] :
s.sym2 = Finset.image Sym2.mk (s ×ˢ s)
theorem Finset.isDiag_mk_of_mem_diag {α : Type u_1} {s : Finset α} [DecidableEq α] {a : α × α} (h : a s.diag) :
(Sym2.mk a).IsDiag
theorem Finset.not_isDiag_mk_of_mem_offDiag {α : Type u_1} {s : Finset α} [DecidableEq α] {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} {s : Finset α} [DecidableEq α] :
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
@[simp]
theorem Finset.sym_zero {α : Type u_1} {s : Finset α} [DecidableEq α] :
s.sym 0 = {}
@[simp]
theorem Finset.sym_succ {α : Type u_1} {s : Finset α} [DecidableEq α] {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} {s : Finset α} [DecidableEq α] {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} {s : Finset α} {a : α} [DecidableEq α] (ha : a s) (n : ) :
Sym.replicate n a s.sym n
theorem Finset.Nonempty.sym {α : Type u_1} {s : Finset α} [DecidableEq α] (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} {s : Finset α} [DecidableEq α] {n : } (h : s.sym n = ) :
s =
@[simp]
theorem Finset.sym_eq_empty {α : Type u_1} {s : Finset α} [DecidableEq α] {n : } :
s.sym n = n 0 s =
@[simp]
theorem Finset.sym_nonempty {α : Type u_1} {s : Finset α} [DecidableEq α] {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} {s : Finset α} {t : Finset α} [DecidableEq α] (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} {s : Finset α} [DecidableEq α] {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} {s : Finset α} [DecidableEq α] {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_apply_fst {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {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} {s : Finset α} {a : α} [DecidableEq α] {n : } (h : as) (m : { x : Sym α n // x (insert a s).sym n }) :
((Finset.symInsertEquiv h) m).snd = (Sym.filterNe a m).snd
@[simp]
theorem Finset.symInsertEquiv_symm_apply_coe {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {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
def Finset.symInsertEquiv {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {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.