Commit 2024-06-22 19:13 2985a848

View on Github →

feat: forward direction of Turán's theorem (#11990) Part of #9317.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Turan.lean

added theorem SimpleGraph.IsTuranMaximal.card_parts

added theorem SimpleGraph.IsTuranMaximal.card_parts_le

added theorem SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card

added theorem SimpleGraph.IsTuranMaximal.degree_eq_of_not_adj

added theorem SimpleGraph.IsTuranMaximal.equivalence_not_adj

added def SimpleGraph.IsTuranMaximal.finpartition

added theorem SimpleGraph.IsTuranMaximal.isEquipartition

added theorem SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph

added theorem SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq

added theorem SimpleGraph.IsTuranMaximal.not_adj_trans

added def SimpleGraph.IsTuranMaximal.setoid

added theorem SimpleGraph.exists_isTuranMaximal

Modified Mathlib/Order/Partition/Finpartition.lean

modified theorem Finpartition.mem_part

added theorem Finpartition.mem_part_iff_part_eq_part

added theorem Finpartition.part_eq_of_mem

modified theorem Finpartition.part_mem