iso — Mathlib

English

Turán-maximality for r is preserved under graph isomorphisms.

Русский

Турэнмаксимация по r сохраняется под изоморфизмами графов.

LaTeX

$$$\text{iso }(G,H):\; G.\text{IsTuranMaximal}(r) \Rightarrow H.\text{IsTuranMaximal}(r)$ when $G \cong H$ and hr>0.$$

Lean4

/-- Turán-maximality with `0 < r` transfers across graph isomorphisms. -/
theorem iso {W : Type*} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (h : G.IsTuranMaximal r) (f : G ≃g H)
    (hr : 0 < r) : H.IsTuranMaximal r :=
  isTuranMaximal_of_iso (h.nonempty_iso_turanGraph.some.comp f.symm) hr

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