card_finset_len — Mathlib

English

For a finite α, the number of k-element subsets of α is binomial(|α|, k).

Русский

Для конечного α число подмножеств размером k равно биномиальному коэффициенту C(|α|, k).

LaTeX

$$$|\\{ s \\subseteq \\alpha \\mid |s| = k \\}| = \\binom{|\\alpha|}{k}$$$

Lean4

@[simp]
theorem card_finset_len [Fintype α] (k : ℕ) : Fintype.card { s : Finset α // #s = k } = Nat.choose (Fintype.card α) k :=
  by simp [Fintype.subtype_card, Finset.card_univ]

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