English
Let G be a simple graph on vertex set V. The distance between two vertices u and v, denoted dist_G(u,v), is the length of the shortest walk from u to v; if no walk exists, the distance is defined to be 0.
Русский
Пусть G — простой граф на множестве вершин V. Расстояние между вершинами u и v, обозначаемое dist_G(u,v), равно длине кратчайшей обходной цепи от u к v; если обхода не существует, расстояние определяется как 0.
LaTeX
$$$$\mathrm{dist}_G(u,v) = \begin{cases} \min\{\mathrm{length}(p) : p \in G.\mathrm{Walk}(u,v)\}, & G.\mathrm{Walk}(u,v) \neq \varnothing \\\\ 0, & G.\mathrm{Walk}(u,v) = \varnothing \end{cases}$$$$
Lean4
/-- The distance between two vertices is the length of the shortest walk between them.
If no such walk exists, this uses the junk value of `0`.
-/
noncomputable def dist (u v : V) : ℕ :=
(G.edist u v).toNat
