exists_path_of_dist — Mathlib

English

If u and v are reachable, there exists p : G.Walk u v such that p.IsPath and p.length = dist_G(u,v).

Русский

Если u и v достижимы, существует p : G.Walk u v такой, что p является путём и length(p) = dist_G(u,v).

LaTeX

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

Lean4

theorem exists_path_of_dist (hr : G.Reachable u v) : ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v :=
  by
  obtain ⟨p, h⟩ := hr.exists_walk_length_eq_dist
  exact ⟨p, p.isPath_of_length_eq_dist h, h⟩

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