English
For any r > 0 there exists a graph G on V that is Turán-maximal for r.
Русский
Для любого r > 0 существует граф G на V, который является Турэнмаксовым для r.
LaTeX
$$$\exists G:\text{SimpleGraph } V,\ \exists (\_ : \text{DecidableRel } G.\mathrm{Adj}),\ G.\mathrm{IsTuranMaximal}(r).$$$
Lean4
theorem exists_isTuranMaximal (hr : 0 < r) : ∃ H : SimpleGraph V, ∃ _ : DecidableRel H.Adj, H.IsTuranMaximal r := by
classical
let c := {H : SimpleGraph V | H.CliqueFree (r + 1)}
have cn : c.toFinset.Nonempty :=
⟨⊥, by
rw [Set.toFinset_setOf, mem_filter_univ]
exact cliqueFree_bot (by cutsat)⟩
obtain ⟨S, Sm, Sl⟩ := exists_max_image c.toFinset (#·.edgeFinset) cn
use S, inferInstance
rw [Set.mem_toFinset] at Sm
refine ⟨Sm, fun I _ cf ↦ ?_⟩
by_cases Im : I ∈ c.toFinset
· convert Sl I Im
· rw [Set.mem_toFinset] at Im
contradiction
