Commit 2026-09-04 11:59 52b284ff

feat(Combinatorics/SimpleGraph/Clique): clique numbers of top and bot (#43096) Some of these hold more generally under [Finite G.edgeSet] rather than [Finite α], but we need better Sym2 cardinality theorems to show it. This is especially obvious for cliqueNum_bot, since it shouldn't need any finiteness assumptions (it always has finitely many edges).