isTuranMaximal_iff_nonempty_iso_turanGraph

English

Let G be a simple graph on a finite vertex set V, with r > 0. Then G is Turán-maximal with respect to forbidding K_{r+1} if and only if G is isomorphic to the Turán graph on |V| vertices with parameter r.

Русский

Пусть G — простной граф на конечном множестве вершин V и r > 0. Тогда G является Турвановой-максимальной по запрету K_{r+1} если и только если G изоморфен графу Турaна на |V| вершинах с параметром r.

LaTeX

$$$\\exists \\phi:\\ G \\cong turanGraph(|V|, r).$$$

Lean4

/-- **Turán's theorem**. `turanGraph n r` is, up to isomorphism, the unique
`r + 1`-cliquefree Turán-maximal graph on `n` vertices. -/
theorem isTuranMaximal_iff_nonempty_iso_turanGraph (hr : 0 < r) :
    G.IsTuranMaximal r ↔ Nonempty (G ≃g turanGraph (Fintype.card V) r) :=
  ⟨fun h ↦ h.nonempty_iso_turanGraph, fun h ↦ isTuranMaximal_of_iso h.some hr⟩

Похожие утверждения