English
Let α be a finite set and 𝒜 a finite family of finite subsets of α. Then 𝒜 is contained in the r-element subsets of α if and only if, when viewed as a set of Finsets, every member of 𝒜 has cardinality r.
Русский
Пусть α—конечное множество и 𝒜 — конечное семейство конечных подмножеств α. Тогда 𝒜 ⊆ {B ⊆ α : |B| = r} тогда же, когда множество элементов 𝒜 (как множество подмножеств α) состоит только из подмножеств размерности r.
LaTeX
$$$ 𝒜 \subseteq \mathrm{powersetCard}\, r\, \mathrm{univ} \ \Longleftrightarrow \ (𝒜 : \mathrm{Set}(\mathrm{Finset}\ \alpha)).\mathrm{Sized}\, r $$$
Lean4
theorem subset_powersetCard_univ_iff : 𝒜 ⊆ powersetCard r univ ↔ (𝒜 : Set (Finset α)).Sized r :=
forall_congr' fun A => by rw [mem_powersetCard_univ, mem_coe]
