edist_eq_sInf — Mathlib

English

The extended distance between vertices equals the infimum of the lengths of all walks from u to v.

Русский

Расстояние в расширенном смысле между вершинами равно инфиму длин всех путей-м Walks от u до v.

LaTeX

$$$ G.edist u v = \mathrm{sInf}(\{ w.length : \mathbb{N}_\infty \mid w \in G.Walk u v \}) $$$

Lean4

theorem edist_eq_sInf : G.edist u v = sInf (Set.range fun w : G.Walk u v ↦ (w.length : ℕ∞)) :=
  rfl

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