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.

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.repeat_mem_sym {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} (ha : a ∈ s) (n : ℕ) :
sym.repeat a n ∈ 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.repeat a n}
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