Commit 2026-01-30 13:30 0ab9ff4c

View on Github →

feat(Combinatorics/SimpleGraph/Clique): avoid Fintype/Finite assumptions where possible (#33253) Also prove G.cliqueNum ≤ G.chromaticNumber without any finiteness assumptions.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

modified theorem SimpleGraph.IsIndepSet.nonempty_mem_compl_mem_edge

modified theorem SimpleGraph.IsMaximumClique.isMaximalClique

modified structure SimpleGraph.IsMaximumClique

modified structure SimpleGraph.IsMaximumIndepSet

modified theorem SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card

modified theorem SimpleGraph.exists_isNClique_cliqueNum

modified theorem SimpleGraph.exists_isNIndepSet_indepNum

modified theorem SimpleGraph.isMaximumClique_compl

modified theorem SimpleGraph.isMaximumClique_iff

modified theorem SimpleGraph.isMaximumIndepSet_compl

modified theorem SimpleGraph.maximumClique_card_eq_cliqueNum

modified theorem SimpleGraph.maximumClique_exists

modified theorem SimpleGraph.maximumIndepSet_exists

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

added theorem SimpleGraph.cliqueNum_le_chromaticNumber