Mathlib.Combinatorics.SimpleGraph.Metric._auxLemma.2

theorem Mathlib.Combinatorics.SimpleGraph.Metric._auxLemma.2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, (G.dist u v = 0) = (u = v ∨ ¬G.Reachable u v)

The theorem `Mathlib.Combinatorics.SimpleGraph.Metric._auxLemma.2` states that for any simple graph `G` of vertices `V` and any two vertices `u` and `v` from `V`, the distance between `u` and `v` in `G` is zero if and only if `u` and `v` are the same vertex or there is no walk in `G` that connects `u` and `v`. Here, the distance between two vertices is defined as the length of the shortest walk between them and two vertices are said to be reachable if there exists a walk between them.

More concisely: The theorem asserts that in a simple graph, the distance between two vertices is zero if and only if they are the same vertex or there is no path connecting them.