Theorems · Theorem · combinatorics

Finset.kruskal_katona

• 1000+ list: Kruskal–Katona theorem

∀ {n r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))},
  Set.Sized r ↑𝒜 → 𝒞.card ≤ 𝒜.card → Finset.Colex.IsInitSeg 𝒞 r → 𝒞.shadow.card ≤ 𝒜.shadow.card

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.

Defined in

Mathlib.Combinatorics.SetFamily.KruskalKatona

Cited by

1 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound