English
The number of k-multisets drawn from an n-element set equals the multichoose number, i.e. |Sym(Fin n, k)| = n multichoose k.
Русский
Число мультимножеств размера k, взятых из множества с n элементами, равно числу multichoose: |Sym(Fin n, k)| = n multichoose k.
LaTeX
$$$\lvert \mathrm{Sym}(\mathrm{Fin}\,n)\,k\rvert = n \cdot\!\! \text{multichoose} \; k$$$
Lean4
theorem card_sym_fin_eq_multichoose : ∀ n k : ℕ, card (Sym (Fin n) k) = multichoose n k
| n, 0 => by simp
| 0, k + 1 => by rw [multichoose_zero_succ]; exact card_eq_zero
| 1, k + 1 => by simp
| n + 2, k + 1 =>
by
rw [multichoose_succ_succ, ← card_sym_fin_eq_multichoose (n + 1) (k + 1), ← card_sym_fin_eq_multichoose (n + 2) k,
add_comm (Fintype.card _), ← card_sum]
refine Fintype.card_congr (Equiv.symm ?_)
apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans
apply Equiv.sumCompl
