English
If G is connected and v and w are adjacent, then dist_G(u,w) equals dist_G(u,v) or dist_G(u,v) ± 1.
Русский
Если граф G связан, то для соседних вершин v и w расстояние от u к w равно расстоянию от u к v или на единицу больше/меньше.
LaTeX
$$$$ G.Connected \Rightarrow G.\mathrm{Adj}(v,w) \Rightarrow \mathrm{dist}_G(u,w) \in \{ \mathrm{dist}_G(u,v), \ \mathrm{dist}_G(u,v) + 1, \ \mathrm{dist}_G(u,v) - 1 \} $$$$
Lean4
theorem diff_dist_adj (hG : G.Connected) (hadj : G.Adj v w) :
G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1 :=
by
have : G.dist v w = 1 := dist_eq_one_iff_adj.mpr hadj
have : G.dist w v = 1 := dist_eq_one_iff_adj.mpr hadj.symm
have : G.dist u w ≤ G.dist u v + G.dist v w := hG.dist_triangle
have : G.dist u v ≤ G.dist u w + G.dist w v := hG.dist_triangle
omega
