Commit 2025-09-01 17:39 1d436f8e

View on Github →

feat(SimpleGraph/FiveWheelLike): add the Andrásfai-Erdős-Sós theorem (#25836) Add the Andrásfai-Erdős-Sós theorem colorable_of_cliqueFree_lt_minDegree which says that an r + 1-cliquefree graph G with sufficiently large minimum degree is r-colorable.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

Modified Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

added theorem SimpleGraph.IsFiveWheelLike.exists_isFiveWheelLike_succ_of_not_adj_le_two

added theorem SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ

added theorem SimpleGraph.colorable_of_cliqueFree_lt_minDegree