English
The Kruskal–Katona theorem for general finite set families.
Русский
Общая формулировка теоремы Крускал-Катона для конечных семей множеств.
LaTeX
$$$|\partial 𝒜| \ge \min(\cdot) \text{(appropriate bound)}$$$
Lean4
/-- The **Kruskal-Katona theorem**.
Given a set family `𝒜` consisting of `r`-sets, and `𝒞` an initial segment of the colex order of the
same size, the shadow of `𝒞` is smaller than the shadow of `𝒜`. In particular, this gives that the
minimum shadow size is achieved by initial segments of colex. -/
theorem kruskal_katona (h𝒜r : (𝒜 : Set (Finset (Fin n))).Sized r) (h𝒞𝒜 : #𝒞 ≤ #𝒜) (h𝒞 : IsInitSeg 𝒞 r) :
#(∂ 𝒞) ≤ #(∂ 𝒜) := by
-- WLOG `|𝒜| = |𝒞|`
obtain ⟨𝒜', h𝒜, h𝒜𝒞⟩ := exists_subset_card_eq h𝒞𝒜
obtain ⟨ℬ, hℬ𝒜, h𝒜ℬ, hℬr, hℬ⟩ :=
UV.kruskal_katona_helper 𝒜'
(h𝒜r.mono (by gcongr))
-- This means that `ℬ` is an initial segment of the same size as `𝒞`. Hence they are equal and
-- we are done.
suffices ℬ = 𝒞 by subst 𝒞; exact hℬ𝒜.trans (by gcongr)
have hcard : #ℬ = #𝒞 := h𝒜ℬ.symm.trans h𝒜𝒞
obtain h𝒞ℬ | hℬ𝒞 := h𝒞.total (UV.isInitSeg_of_compressed hℬr hℬ)
· exact (eq_of_subset_of_card_le h𝒞ℬ hcard.le).symm
· exact eq_of_subset_of_card_le hℬ𝒞 hcard.ge
