exists_walk_length_eq_dist — Mathlib

English

If u and v are reachable in G, there exists a walk p from u to v whose length equals the distance dist_G(u,v).

Русский

Если вершины u и v достижимы в графе G, существует обход (путь) p от u к v такой, что длина p равна расстоянию dist_G(u,v).

LaTeX

$$$$ G.\mathrm{Reachable}(u,v) \Rightarrow \exists p : G.\mathrm{Walk}(u,v), \mathrm{length}(p) = \mathrm{dist}_G(u,v) $$$$

Lean4

protected theorem exists_walk_length_eq_dist (hr : G.Reachable u v) : ∃ p : G.Walk u v, p.length = G.dist u v :=
  dist_eq_sInf ▸ Nat.sInf_mem (Set.range_nonempty_iff_nonempty.mpr hr)

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