Symmetric powers of a finset #
This file defines the symmetric powers of a finset as finset (sym α n)
and finset (sym2 α)
.
Main declarations #
finset.sym
: The symmetric power of a finset.s.sym n
is all the multisets of cardinalityn
whose elements are ins
.finset.sym2
: The symmetric square of a finset.s.sym2
is all the pairs whose elements are ins
.
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]
Lifts a finset to sym2 α
. s.sym2
is the finset of all pairs with elements in s
.
Equations
- s.sym2 = finset.image quotient.mk (s ×ˢ s)
@[simp]
@[simp]
@[simp]
@[protected]
Alias of the reverse direction of finset.sym2_nonempty
.
@[simp]
@[simp]
@[simp]
@[simp]
@[protected]
Lifts a finset to sym α n
. s.sym n
is the finset of all unordered tuples of cardinality n
with elements in s
.
@[simp]
@[simp]
theorem
finset.repeat_mem_sym
{α : Type u_1}
[decidable_eq α]
{s : finset α}
{a : α}
(ha : a ∈ s)
(n : ℕ) :
sym.repeat a n ∈ s.sym 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 = ∅) :
@[simp]
@[simp]