Commit 2025-04-07 08:31 eb0f6a5e

View on Github →

feat(Combinatorics/SimpleGraph): add facts about cliques and colorings of completeMultipartiteGraph (#21479) Add basic lemmas about cliques and chromatic number of completeMultipartiteGraph. In particular if a completeMultipartiteGraph is CliqueFree n then it is (n - 1) - colorable. This last result is needed for the Andrasfai-Erdos-Sos theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_infinite

added theorem SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card

added theorem SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_enatCard

added def SimpleGraph.completeMultipartiteGraph.topEmbedding

added theorem SimpleGraph.not_cliqueFree_zero

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

added theorem SimpleGraph.completeMultipartiteGraph.chromaticNumber

added theorem SimpleGraph.completeMultipartiteGraph.colorable

added theorem SimpleGraph.completeMultipartiteGraph.colorable_of_cliqueFree

added def SimpleGraph.completeMultipartiteGraph.coloring

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean