isTuranMaximal_turanGraph — Mathlib

English

For 0 < r, turanGraph(n,r) is Turán-maximal for r.

Русский

Для 0 < r граф Турэна является Турэнмаксимационным для r.

LaTeX

$$$\text{isTuranMaximal_turanGraph}(n,r): 0 < r \Rightarrow (\mathrm{turanGraph}(n,r)).\mathrm{IsTuranMaximal}(r).$$$

Lean4

/-- For `0 < r`, `turanGraph n r` is Turán-maximal. -/
theorem isTuranMaximal_turanGraph (hr : 0 < r) : (turanGraph n r).IsTuranMaximal r :=
  isTuranMaximal_of_iso Iso.refl hr

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