card_le — Mathlib

English

If 𝒜 is a family of Finset α whose elements all have size r, then the total number of elements of 𝒜 is at most the binomial coefficient choose(|α|, r).

Русский

Если 𝒜 — семейство подмножеств α, все элементы которого имеют размер r, то число элементов в 𝒜 не превосходит биномиального коэффициента C(|α|, r).

LaTeX

$$# 𝒜 ≤ (|α| choose r)$$

Lean4

theorem _root_.Set.Sized.card_le (h𝒜 : (𝒜 : Set (Finset α)).Sized r) : #𝒜 ≤ (Fintype.card α).choose r :=
  by
  rw [Fintype.card, ← card_powersetCard]
  exact card_le_card (subset_powersetCard_univ_iff.mpr h𝒜)

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