English
As above, Turán maximal graphs are isomorphic to the Turán template graph.
Русский
Как указано выше, Турэнмаксима-льные графы изоморфны шаблонному графу Турэна.
LaTeX
$$$(\text{same content as 86752})$$$
Lean4
/-- **Turán's theorem**, forward direction.
Any `r + 1`-cliquefree Turán-maximal graph on `n` vertices is isomorphic to `turanGraph n r`. -/
theorem nonempty_iso_turanGraph : Nonempty (G ≃g turanGraph (Fintype.card V) r) := by
classical
obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
intro a b
simp_rw [turanGraph, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
rw [← h.not_adj_iff_part_eq] at this
rw [← not_iff_not, not_ne_iff, this, card_parts]
rcases le_or_gt r (Fintype.card V) with c | c
· rw [min_eq_right c]; rfl
· have lc : ∀ x, zm ⟨x, _⟩ < Fintype.card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b), ← Nat.mod_eq_of_lt ((lc a).trans c), ←
Nat.mod_eq_of_lt ((lc b).trans c)];
rfl
