English
The shatterer size is bounded by a sum over k ≤ 𝒜.vcDim of binomial(Fintype.card α, k).
Русский
Размер шаттерера ограничен суммой по k≤𝒜.vcDim от сочетаний(|α|, k).
LaTeX
$$[Fintype α] ⟦ #𝒜.shatterer ≤ ∑_{k ≤ 𝒜.vcDim} (|α| choose k) ⟧$$
Lean4
/-- The **Sauer-Shelah lemma**. -/
theorem card_shatterer_le_sum_vcDim [Fintype α] : #𝒜.shatterer ≤ ∑ k ∈ Iic 𝒜.vcDim, (Fintype.card α).choose k :=
by
simp_rw [← card_univ, ← card_powersetCard]
refine (card_le_card fun s hs ↦ mem_biUnion.2 ⟨#s, ?_⟩).trans card_biUnion_le
exact ⟨mem_Iic.2 (mem_shatterer.1 hs).card_le_vcDim, mem_powersetCard_univ.2 rfl⟩