exists_walk_of_dist_ne_zero — Mathlib

English

If dist_G(u,v) ≠ 0, then there exists a walk p from u to v with length equal to dist_G(u,v).

Русский

Если dist_G(u,v) ≠ 0, то существует обход p от u к v такой, что length(p) = dist_G(u,v).

LaTeX

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

Lean4

theorem exists_walk_of_dist_ne_zero (h : G.dist u v ≠ 0) : ∃ p : G.Walk u v, p.length = G.dist u v :=
  (Reachable.of_dist_ne_zero h).exists_walk_length_eq_dist

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