English
There are min(n,r) parts in a Turán-maximal graph on n vertices.
Русский
В графе Турэна на n вершинах имеется min(n,r) частей.
LaTeX
$$$\#h.finpartition.parts = \min(\mathrm{card}(V), r).$$$
Lean4
/-- The parts of a Turán-maximal graph form an equipartition. -/
theorem isEquipartition [DecidableEq V] : h.finpartition.IsEquipartition :=
by
set fp := h.finpartition
by_contra hn
rw [Finpartition.not_isEquipartition] at hn
obtain ⟨large, hl, small, hs, ineq⟩ := hn
obtain ⟨w, hw⟩ := fp.nonempty_of_mem_parts hl
obtain ⟨v, hv⟩ := fp.nonempty_of_mem_parts hs
apply absurd h
rw [IsTuranMaximal]; push_neg; intro cf
use G.replaceVertex v w, inferInstance, cf.replaceVertex v w
have large_eq := fp.part_eq_of_mem hl hw
have small_eq := fp.part_eq_of_mem hs hv
have ha : G.Adj v w := by
by_contra hn; rw [h.not_adj_iff_part_eq, small_eq, large_eq] at hn
rw [hn] at ineq; omega
rw [G.card_edgeFinset_replaceVertex_of_adj ha, degree_eq_card_sub_part_card h, small_eq,
degree_eq_card_sub_part_card h, large_eq]
have : #large ≤ Fintype.card V := by simpa using card_le_card large.subset_univ
cutsat
