mathlib3 documentation

data.finset.sym

Symmetric powers of a finset #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

theorem finset.is_diag_mk_of_mem_diag {α : Type u_1} [decidable_eq α] {s : finset α} {a : α × α} (h : a s.diag) :
theorem finset.not_is_diag_mk_of_mem_off_diag {α : Type u_1} [decidable_eq α] {s : finset α} {a : α × α} (h : a s.off_diag) :
@[protected]
def finset.sym2 {α : Type u_1} [decidable_eq α] (s : finset α) :

Lifts a finset to sym2 α. s.sym2 is the finset of all pairs with elements in s.

Equations
@[simp]
theorem finset.mem_sym2_iff {α : Type u_1} [decidable_eq α] {s : finset α} {m : sym2 α} :
m s.sym2 (a : α), a m a s
theorem finset.mk_mem_sym2_iff {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
(a, b) s.sym2 a s b s
@[simp]
theorem finset.sym2_empty {α : Type u_1} [decidable_eq α] :
@[simp]
theorem finset.sym2_eq_empty {α : Type u_1} [decidable_eq α] {s : finset α} :
@[simp]
theorem finset.sym2_nonempty {α : Type u_1} [decidable_eq α] {s : finset α} :
@[protected]
theorem finset.nonempty.sym2 {α : Type u_1} [decidable_eq α] {s : finset α} :

Alias of the reverse direction of finset.sym2_nonempty.

@[simp]
@[simp]
theorem finset.sym2_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a}.sym2 = {sym2.diag a}
@[simp]
theorem finset.diag_mem_sym2_iff {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
@[simp]
theorem finset.sym2_mono {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s t) :
@[protected]
def finset.sym {α : Type u_1} [decidable_eq α] (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} [decidable_eq α] {s : finset α} :
s.sym 0 = {}
@[simp]
theorem finset.sym_succ {α : Type u_1} [decidable_eq α] {s : finset α} {n : } :
s.sym (n + 1) = s.sup (λ (a : α), finset.image (sym.cons a) (s.sym n))
@[simp]
theorem finset.mem_sym_iff {α : Type u_1} [decidable_eq α] {s : finset α} {n : } {m : sym α n} :
m s.sym n (a : α), a m a s
@[simp]
theorem finset.sym_empty {α : Type u_1} [decidable_eq α] (n : ) :
.sym (n + 1) =
theorem finset.replicate_mem_sym {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (ha : a s) (n : ) :
@[protected]
theorem finset.nonempty.sym {α : Type u_1} [decidable_eq α] {s : finset α} (h : s.nonempty) (n : ) :
@[simp]
theorem finset.sym_singleton {α : Type u_1} [decidable_eq α] (a : α) (n : ) :
{a}.sym n = {sym.replicate n a}
theorem finset.eq_empty_of_sym_eq_empty {α : Type u_1} [decidable_eq α] {s : finset α} {n : } (h : s.sym n = ) :
s =
@[simp]
theorem finset.sym_eq_empty {α : Type u_1} [decidable_eq α] {s : finset α} {n : } :
s.sym n = n 0 s =
@[simp]
theorem finset.sym_nonempty {α : Type u_1} [decidable_eq α] {s : finset α} {n : } :
@[simp]
theorem finset.sym_univ {α : Type u_1} [decidable_eq α] [fintype α] (n : ) :
@[simp]
theorem finset.sym_mono {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s t) (n : ) :
s.sym n t.sym n
@[simp]
theorem finset.sym_inter {α : Type u_1} [decidable_eq α] (s t : finset α) (n : ) :
(s t).sym n = s.sym n t.sym n
@[simp]
theorem finset.sym_union {α : Type u_1} [decidable_eq α] (s t : finset α) (n : ) :
s.sym n t.sym n (s t).sym n
theorem finset.sym_fill_mem {α : Type u_1} [decidable_eq α] {s : finset α} {n : } (a : α) {i : fin (n + 1)} {m : sym α (n - i)} (h : m s.sym (n - i)) :
theorem finset.sym_filter_ne_mem {α : Type u_1} [decidable_eq α] {s : finset α} {n : } {m : sym α n} (a : α) (h : m s.sym n) :
def finset.sym_insert_equiv {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} {n : } (h : a s) :
((has_insert.insert a s).sym n) Σ (i : fin (n + 1)), (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
@[simp]
theorem finset.sym_insert_equiv_symm_apply_coe {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} {n : } (h : a s) (m : Σ (i : fin (n + 1)), (s.sym (n - i))) :
@[simp]
theorem finset.sym_insert_equiv_apply_fst {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} {n : } (h : a s) (m : ((has_insert.insert a s).sym n)) :
@[simp]
theorem finset.sym_insert_equiv_apply_snd_coe {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} {n : } (h : a s) (m : ((has_insert.insert a s).sym n)) :