Commit 2024-08-24 13:23 bf434437

View on Github →

feat: The Kruskal-Katona theorem (#15000) Prove the Kruskal-Katona theorem. From LeanCamCombi

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/KruskalKatona.lean

added theorem Finset.Colex.shadow_initSeg

added theorem Finset.UV.isInitSeg_of_compressed

added theorem Finset.UV.toColex_compress_lt_toColex

added theorem Finset.iterated_kk

added theorem Finset.kruskal_katona

Modified Mathlib/Combinatorics/SetFamily/Shadow.lean

added theorem Finset.shadow_mono