dist_eq_one_iff_adj — Mathlib

English

The distance between u and v is 1 if and only if u and v are adjacent.

Русский

Расстояние между u и v равно 1 тогда и только тогда, когда вершины смежны.

LaTeX

$$$$ \mathrm{dist}_G(u,v) = 1 \iff G.\mathrm{Adj}(u,v) $$$$

Lean4

/-- The distance between vertices is equal to `1` if and only if these vertices are adjacent.
-/
@[simp]
theorem dist_eq_one_iff_adj : G.dist u v = 1 ↔ G.Adj u v :=
  by
  rw [dist, ENat.toNat_eq_iff, ENat.coe_one, edist_eq_one_iff_adj]
  decide

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