adj_replaceVertex_iff_of_ne_left — Mathlib

English

If w ≠ t, then (G.replaceVertex s t).Adj s w iff G.Adj s w.

Русский

Если w ≠ t, то (G.replaceVertex s t).Adj s w равно G.Adj s w.

LaTeX

$$$ {w} \neq t \Rightarrow (G.replaceVertex s t).Adj(s,w) \iff G.Adj(s,w) $$$

Lean4

/-- Except possibly for `t`, the neighbours of `s` in `G.replaceVertex s t` are its neighbours in
`G`. -/
theorem adj_replaceVertex_iff_of_ne_left {w : V} (hw : w ≠ t) : (G.replaceVertex s t).Adj s w ↔ G.Adj s w := by
  simp [replaceVertex, hw]

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