mathlib documentation

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.

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 ma 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]
theorem finset.sym2_univ {α : Type u_1} [decidable_eq α] [fintype α] :
@[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 ma s
@[simp]
theorem finset.sym_empty {α : Type u_1} [decidable_eq α] (n : ) :
.sym (n + 1) =
theorem finset.repeat_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.repeat a n}
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