adj_replaceVertex_iff_of_ne — Mathlib

English

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

Русский

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

LaTeX

$$$ v \neq t \land w \neq t \Rightarrow (G.replaceVertex s t).Adj(v,w) \iff G.Adj(v,w) $$$

Lean4

/-- Adjacency in `G.replaceVertex s t` which does not involve `t` is the same as that of `G`. -/
theorem adj_replaceVertex_iff_of_ne {v w : V} (hv : v ≠ t) (hw : w ≠ t) : (G.replaceVertex s t).Adj v w ↔ G.Adj v w :=
  by simp [replaceVertex, hv, hw]

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