Finset.card_sym2
theorem Finset.card_sym2 : ∀ {α : Type u_1} (s : Finset α), s.sym2.card = (s.card + 1).choose 2
This theorem, known as the "Finset stars and bars" for the case `n = 2`, states that for any finite set `s`, the number of ways to form unordered pairs (which is represented by `s.sym2.card`) is equal to the binomial coefficient "choose 2" of the cardinality of set `s` plus one. In other words, if `s` is a finite set, the number of 2-element combinations in `s` is given by the formula $\binom{s.card + 1}{2}$.
More concisely: The number of unordered pairs in a finite set equals the binomial coefficient of its cardinality plus one.
|
Finset.Nonempty.sym2
theorem Finset.Nonempty.sym2 : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → s.sym2.Nonempty
This theorem, `Finset.Nonempty.sym2`, states that for any type `α` and any finite set `s` of this type, if the set `s` is nonempty, then the symmetric square of `s` is also nonempty. The symmetric square of a set is the set of all unordered pairs of its elements.
More concisely: If `s` is a finite, nonempty set, then the symmetric square of `s` is a nonempty set.
|
Finset.sym2_val
theorem Finset.sym2_val : ∀ {α : Type u_1} (s : Finset α), s.sym2.val = s.val.sym2
This theorem states that for every type `α` and a finite set `s` of type `α`, the value of the set of all unordered pairs of elements from `s` (obtained through `Finset.sym2`) is equal to the multiset of all unordered pairs of elements from the multiset `s.val` (obtained through `Multiset.sym2`). Here, `s.val` refers to the underlying multiset of the finite set `s`. In essence, it claims that the transformation of a finite set to a set of its unordered pairs is equivalent to the transformation of its underlying multiset to a multiset of its unordered pairs.
More concisely: For every finite multiset `s` of type `α`, the multiset of unordered pairs of elements in `s` (obtained through `Multiset.sym2`) is equal to the set of unordered pairs of elements from the underlying finite set of `s` (obtained through `Finset.sym2`).
|
Finset.mem_sym_iff
theorem Finset.mem_sym_iff :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {n : ℕ} {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s := by
sorry
The theorem `Finset.mem_sym_iff` states that for any given type `α` equipped with decidable equality, a `Finset` `s` of type `α`, a natural number `n`, and a symmetric power `m` of type `Sym α n`, `m` is an element of the symmetric power `Finset.sym s n` if and only if every element `a` in `m` is also an element of `s`. In other words, an unordered tuple `m` is in the `n`-th symmetric power of the set `s` if and only if all of its elements are in `s`.
More concisely: For any type `α` with decidable equality, a finite set `s` of `α`, and a natural number `n`, the element `m` is in the `n`-th symmetric power of `Finset.sym s` if and only if all elements in `m` are in `s`.
|