dist_eq_zero_iff_eq_or_not_reachable

English

The distance is zero exactly when the vertices coincide or there is no path between them.

Русский

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

LaTeX

$$$$ \mathrm{dist}_G(u,v) = 0 \iff u = v \lor \neg G.\mathrm{Reachable}(u,v) $$$$

Lean4

@[simp]
theorem dist_eq_zero_iff_eq_or_not_reachable : G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v := by
  simp [dist_eq_sInf, Nat.sInf_eq_zero, Reachable]

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