Commit 2024-03-23 07:52 1ed91c39

View on Github →

feat: definition and properties of the Turán graph (#9645) The first part of the main file in #9317.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

modified theorem SimpleGraph.edgeFinset_sup

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

modified theorem SimpleGraph.card_edgeFinset_sup_edge

modified theorem SimpleGraph.edgeFinset_sup_edge

Created Mathlib/Combinatorics/SimpleGraph/Turan.lean

added theorem SimpleGraph.IsTuranMaximal.le_iff_eq

added def SimpleGraph.IsTuranMaximal

added theorem SimpleGraph.isTuranMaximal_turanGraph

added theorem SimpleGraph.not_cliqueFree_of_isTuranMaximal

added def SimpleGraph.turanGraph

added theorem SimpleGraph.turanGraph_cliqueFree

added theorem SimpleGraph.turanGraph_eq_top

added theorem SimpleGraph.turanGraph_zero