exists_walk_length_eq_edist — Mathlib

English

If G.Reachable u v, there exists a walk p from u to v whose length equals G.edist u v.

Русский

Если вершины u и v связаны, существует путь (Walk) от u к v, длина которого равна edist u v.

LaTeX

$$$ G.Reachable u v \Rightarrow \exists p : G.Walk u v, p.length = G.edist u v $$$

Lean4

protected theorem exists_walk_length_eq_edist (hr : G.Reachable u v) : ∃ p : G.Walk u v, p.length = G.edist u v :=
  csInf_mem <| Set.range_nonempty_iff_nonempty.mpr hr

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