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.

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

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

Equations
source
@[simp]
theorem finset.mem_sym2_iff {α : Type u_1} [decidable_eq α] {s : finset α} {m : sym2 α} :
m ∈ s.sym2 ↔ ∀ (a : α), a ∈ m → a ∈ s
source
theorem finset.mk_mem_sym2_iff {α : Type u_1} [decidable_eq α] {s : finset α} {a b : α} :
⟦(a, b)⟧ ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
source
@[simp]
theorem finset.sym2_empty {α : Type u_1} [decidable_eq α] :
∅.sym2 = ∅
source
@[simp]
theorem finset.sym2_eq_empty {α : Type u_1} [decidable_eq α] {s : finset α} :
s.sym2 = ∅ ↔ s = ∅
source
@[simp]
theorem finset.sym2_nonempty {α : Type u_1} [decidable_eq α] {s : finset α} :
s.sym2.nonempty ↔ s.nonempty
source
@[protected]
theorem finset.nonempty.sym2 {α : Type u_1} [decidable_eq α] {s : finset α} :
s.nonempty → s.sym2.nonempty

Alias of the reverse direction of finset.sym2_nonempty.

source
@[simp]
theorem finset.sym2_univ {α : Type u_1} [decidable_eq α] [fintype α] :
finset.univ.sym2 = finset.univ
source
@[simp]
theorem finset.sym2_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a}.sym2 = {sym2.diag a}
source
@[simp]
theorem finset.diag_mem_sym2_iff {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
sym2.diag a ∈ s.sym2 ↔ a ∈ s
source
@[simp]
theorem finset.sym2_mono {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) :
s.sym2 ⊆ t.sym2
source
theorem finset.image_diag_union_image_off_diag {α : Type u_1} [decidable_eq α] {s : finset α} :
finset.image quotient.mk s.diag ∪ finset.image quotient.mk s.off_diag = s.sym2
source
@[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
source
@[simp]
theorem finset.sym_zero {α : Type u_1} [decidable_eq α] {s : finset α} :
s.sym 0 = {∅}
source
@[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))
source
@[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
source
@[simp]
theorem finset.sym_empty {α : Type u_1} [decidable_eq α] (n : ℕ) :
∅.sym (n + 1) = ∅
source
theorem finset.replicate_mem_sym {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (ha : a ∈ s) (n : ℕ) :
sym.replicate n a ∈ s.sym n
source
@[protected]
theorem finset.nonempty.sym {α : Type u_1} [decidable_eq α] {s : finset α} (h : s.nonempty) (n : ℕ) :
(s.sym n).nonempty
source
@[simp]
theorem finset.sym_singleton {α : Type u_1} [decidable_eq α] (a : α) (n : ℕ) :
{a}.sym n = {sym.replicate n a}
source
theorem finset.eq_empty_of_sym_eq_empty {α : Type u_1} [decidable_eq α] {s : finset α} {n : ℕ} (h : s.sym n = ∅) :
s = ∅
source
@[simp]
theorem finset.sym_eq_empty {α : Type u_1} [decidable_eq α] {s : finset α} {n : ℕ} :
s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅
source
@[simp]
theorem finset.sym_nonempty {α : Type u_1} [decidable_eq α] {s : finset α} {n : ℕ} :
(s.sym n).nonempty ↔ n = 0 ∨ s.nonempty
source
@[simp]
theorem finset.sym_univ {α : Type u_1} [decidable_eq α] [fintype α] (n : ℕ) :
finset.univ.sym n = finset.univ
source
@[simp]
theorem finset.sym_mono {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) (n : ℕ) :
s.sym n ⊆ t.sym n
source
@[simp]
theorem finset.sym_inter {α : Type u_1} [decidable_eq α] (s t : finset α) (n : ℕ) :
(s ∩ t).sym n = s.sym n ∩ t.sym n
source
@[simp]
theorem finset.sym_union {α : Type u_1} [decidable_eq α] (s t : finset α) (n : ℕ) :
s.sym n ∪ t.sym n ⊆ (s ∪ t).sym n
source
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)) :
sym.fill a i m ∈ (has_insert.insert a s).sym n
source
theorem finset.sym_filter_ne_mem {α : Type u_1} [decidable_eq α] {s : finset α} {n : ℕ} {m : sym α n} (a : α) (h : m ∈ s.sym n) :
(sym.filter_ne a m).snd ∈ (s.erase a).sym (n - ↑((sym.filter_ne a m).fst))
source
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
source
@[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))) :
↑(⇑((finset.sym_insert_equiv h).symm) m) = sym.fill a m.fst m.snd.val
source
@[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)) :
(⇑(finset.sym_insert_equiv h) m).fst = (sym.filter_ne a m.val).fst
source
@[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)) :
↑((⇑(finset.sym_insert_equiv h) m).snd) = (sym.filter_ne a m.val).snd