Sym.card_sym_eq_multichoose
theorem Sym.card_sym_eq_multichoose :
∀ (α : Type u_3) (k : ℕ) [inst : Fintype α] [inst_1 : Fintype (Sym α k)],
Fintype.card (Sym α k) = (Fintype.card α).multichoose k
This theorem states that for any finite type `α` with cardinality `n`, the cardinality of the `k`th symmetric power of `α` is equal to the multichoose of `n` and `k`. In mathematical terms, if we let `α` be a set with `n` elements, then the number of ways to choose (with replacement) `k` elements from `α` is equal to the number of `k`-tuples of `α` considered up to permutation.
More concisely: For a finite type `α` with cardinality `n`, the number of ways to choose `k` elements from `α` with replacement is equal to the multichoose of `n` and `k`, denoted as `(n choose k)`.
|
Sym2.card_image_offDiag
theorem Sym2.card_image_offDiag :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), (Finset.image Sym2.mk s.offDiag).card = s.card.choose 2
The theorem `Sym2.card_image_offDiag` states that for any finite set `s` of a type `α` that has decidable equality, the cardinality of the forward image of the off-diagonal part of `s` under the function `Sym2.mk` (which maps pairs to symmetric pairs) is equal to the binomial coefficient "s choose 2". This is due to the fact that each element of symmetric pairs from `s` that isn't on the diagonal originates from exactly two pairs: `(x, y)` and `(y, x)`.
More concisely: The cardinality of the image of the off-diagonal part of a finite set under the `Sym2.mk` function equals the binomial coefficient of the set's cardinality.
|
Sym.card_sym_eq_choose
theorem Sym.card_sym_eq_choose :
∀ {α : Type u_3} [inst : Fintype α] (k : ℕ) [inst_1 : Fintype (Sym α k)],
Fintype.card (Sym α k) = (Fintype.card α + k - 1).choose k
The theorem `Sym.card_sym_eq_choose` is also known as the "stars and bars" lemma in combinatorics. This lemma states that for any finite type `α` and any natural number `k`, the cardinality (or number of elements) of the nth symmetric power of `α`, denoted as `Sym α k`, is equal to the binomial coefficient "choose" `(card α + k - 1) choose k`. The nth symmetric power of `α` represents the set of all n-tuples of `α` up to permutation. The term `Fintype.card α + k - 1` refers to the total number of symbols (stars and bars) used to form the n-tuples, and `k` is the number of ways to choose k elements from the set. This theorem provides a mathematical way to calculate the number of ways to distribute `k` identical items among `card α` distinct groups.
More concisely: The cardinality of the nth symmetric power of a finite type equals the binomial coefficient "choose" (number of elements + n - 1) over n.
|
Sym2.card
theorem Sym2.card : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card (Sym2 α) = (Fintype.card α + 1).choose 2 := by
sorry
The theorem `Sym2.card` states that for any finite type `α`, the number of elements in the symmetric square of `α` (i.e., the set of unordered pairs of elements from `α`) is equal to "choose 2" of the size of `α` plus 1. In mathematical notation, if |α| denotes the number of elements in `α`, then the number of unordered pairs is given by (|α| + 1 choose 2). This is a special case of the "stars and bars" problem in combinatorics where `n = 2`.
More concisely: The number of unordered pairs in a finite set of size `n` is equal to the binomial coefficient `(n + 1) choose 2`.
|
Sym2.card_image_diag
theorem Sym2.card_image_diag :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), (Finset.image Sym2.mk s.diag).card = s.card
This theorem states that for any set `s` of a certain type `α`, where `α` has decidable equality, the cardinality (or size) of the forward image of the diagonal of `s` under the constructor for `Sym2` (i.e., `Sym2.mk`) is equal to the cardinality of `s`. In simpler terms, it says that when you construct a set of pairs from `s` where each element is paired with itself and then map each pair to an element of `Sym2 α`, the number of elements in the resulting set is the same as the original set `s`.
More concisely: The cardinality of the set of self-paired elements in a set `s` of type `α` with decidable equality, and the cardinality of the image of this set under the `Sym2` constructor, are equal.
|