degree_eq_of_not_adj — Mathlib

English

In a Turán-maximal graph, if two vertices s and t are not adjacent, then their degrees are equal.

Русский

В сутурэнмакситевом графе, если две вершины s и t не смежны, их степеней равны.

LaTeX

$$$G\text{ IsTuranMaximal } r \wedge \neg G.Adj s t \Rightarrow G.\deg(s) = G.\deg(t).$$$

Lean4

/-- In a Turán-maximal graph, non-adjacent vertices have the same degree. -/
theorem degree_eq_of_not_adj (h : G.IsTuranMaximal r) (hn : ¬G.Adj s t) : G.degree s = G.degree t :=
  by
  rw [IsTuranMaximal] at h; contrapose! h; intro cf
  wlog hd : G.degree t < G.degree s generalizing G t s
  · replace hd : G.degree s < G.degree t := lt_of_le_of_ne (le_of_not_gt hd) h
    exact this (by rwa [adj_comm] at hn) hd.ne' cf hd
  classical
  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
  cutsat

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