isTuranMaximal_of_iso — Mathlib

English

If a graph is isomorphic to a Turán graph and r>0, then the graph is Turán-maximal.

Русский

Если граф изоморфен графу Турэна и r>0, то граф является Турэнмаксимационным.

LaTeX

$$$\text{isTuranMaximal_of_iso} : (\exists f:\ G \cong_g \mathrm{turanGraph}(n,r)) \Rightarrow G.\mathrm{IsTuranMaximal}(r)$ for hr>0.$$

Lean4

/-- **Turán's theorem**, reverse direction.

Any graph isomorphic to `turanGraph n r` is itself Turán-maximal if `0 < r`. -/
theorem isTuranMaximal_of_iso (f : G ≃g turanGraph n r) (hr : 0 < r) : G.IsTuranMaximal r :=
  by
  obtain ⟨J, _, j⟩ := exists_isTuranMaximal (V := V) hr
  obtain ⟨g⟩ := j.nonempty_iso_turanGraph
  rw [f.card_eq, Fintype.card_fin] at g
  use (turanGraph_cliqueFree (n := n) hr).comap f, fun H _ cf ↦ (f.symm.comp g).card_edgeFinset_eq ▸ j.2 H cf

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