card_powersetCard — Mathlib

English

The number of n-element submultisets of s equals the binomial coefficient choose(card s, n).

Русский

Число n-элементных подмножств s равно биномиальному коэффициенту choose(card(s), n).

LaTeX

$$$\operatorname{card}(\mathrm{powersetCard}\ n\ s) = \binom{\operatorname{card}(s)}{n}$$$

Lean4

@[simp]
theorem card_powersetCard (n : ℕ) (s : Multiset α) : card (powersetCard n s) = Nat.choose (card s) n :=
  Quotient.inductionOn s <| by simp [powersetCard_coe]

Похожие утверждения