not_adj_replaceVertex_same — Mathlib

English

There is never an edge between the replaced vertex and itself after replacing s by t: (G.replaceVertex s t).Adj s t is false.

Русский

После замены вершины s на t ребро между s и t не существует: (G.replaceVertex s t).Adj s t ложь.

LaTeX

$$$ \neg \big( (G.replaceVertex s t).Adj(s,t) \big)$$$

Lean4

/-- There is never an `s-t` edge in `G.replaceVertex s t`. -/
theorem not_adj_replaceVertex_same : ¬(G.replaceVertex s t).Adj s t := by simp [replaceVertex]

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