Existing in Mathlib · Combinatorics
Kruskal–Katona Theorem
Take a finite r-uniform family 𝒜 and a colex initial segment 𝒞 of r-element subsets with no more members than 𝒜. Form every distinct set obtained by deleting exactly one element from a member of each family. The colex family produces no more such one-step deletions than 𝒜.
- extremal set theory
- uniform set families
- colex order
- immediate shadows
- set-family compression
Exact theorem
Exact Mathlib statement
theorem Finset.kruskal_katona {n r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h𝒜r : (𝒜 : Set (Finset (Fin n))).Sized r) (h𝒞𝒜 : #𝒞 ≤ #𝒜) (h𝒞 : Finset.Colex.IsInitSeg 𝒞 r) : #(∂ 𝒞) ≤ #(∂ 𝒜)The theorem at a glance
Kruskal–Katona Theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Kruskal–Katona Theorem at a glance
Detailed visual description
Unlabelled three-bead family tiles and two-bead shadow tiles introduce one-element deletion without pretending to enumerate the general theorem. The dominant panel separates the size premise from the immediate-shadow conclusion. The source-bound ribbon then matches cardinality, compresses without growing the shadow, decreases a terminating family measure, and identifies the fully compressed endpoint with the colex initial segment.
Statement structure
From hypotheses to conclusion
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Kruskal–Katona Theorem — scientific diagram
Detailed visual description
This page indexes Mathlib’s colex-initial-segment form of the Kruskal–Katona theorem for finite families of subsets of Fin n. The comparison family 𝒜 is r-uniform, 𝒞 is a colex initial segment of the r-subsets, and #𝒞 may be smaller than #𝒜. The selected endpoint compares only the cardinalities of their immediate one-element-deletion shadows. It is not the later iterated-shadow theorem, the Lovász/binomial formulation, an equality-case classification, a uniqueness theorem, or an algorithm.
Why it matters
A mathematical landmark
Kruskal–Katona is a foundational sharp extremal theorem for uniform set families. It identifies colex initial segments as canonical shadow minimizers and its Mathlib source exposes a particularly teachable route through compressions, a strictly decreasing family measure, and a terminal colex family.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib’s colex-initial-segment form of the Kruskal–Katona theorem for finite families of subsets of Fin n. The comparison family 𝒜 is r-uniform, 𝒞 is a colex initial segment of the r-subsets, and #𝒞 may be smaller than #𝒜. The selected endpoint compares only the cardinalities of their immediate one-element-deletion shadows. It is not the later iterated-shadow theorem, the Lovász/binomial formulation, an equality-case classification, a uniqueness theorem, or an algorithm.
- ProofAtlas did not originate the Kruskal–Katona theorem or Mathlib’s declaration.
- The selected declaration compares immediate shadows, not iterated shadows.
- It is not the Lovász or closed binomial-expansion formulation.
- It does not classify equality cases or assert a unique minimizing family.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
Finset.kruskal_katonain mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.kruskal-katona-theorem.v001