card_shatterer_le_sum_vcDim — Mathlib

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⟩

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