Commit 2026-08-12 12:06 4f8cd4ff

View on Github →

feat: Turán numbers and their strict monotonicity (#38200) strictMonoOn_turanNumber was initially proved by @Aristotle-Harmonic, then hand-polished.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean

deleted theorem SimpleGraph.card_edgeFinset_turanGraph

deleted theorem SimpleGraph.card_edgeFinset_turanGraph_add

deleted theorem SimpleGraph.mul_card_edgeFinset_turanGraph_le

added theorem SimpleGraph.mul_turanNumber_le

added theorem SimpleGraph.strictMonoOn_turanNumber

added theorem SimpleGraph.turanGraph_one

modified theorem SimpleGraph.turanGraph_zero

added theorem SimpleGraph.turanNumber_add

added theorem SimpleGraph.turanNumber_eq

added theorem SimpleGraph.turanNumber_three

added theorem SimpleGraph.turanNumber_two