exists_path_of_dist — Mathlib

English

If G is connected, for any u and v there exists p : G.Walk u v such that p.IsPath and p.length = dist_G(u,v).

Русский

Если G связан, для любых вершин u и v существует путь p : G.Walk u v, такой что p — путь и length(p) = dist_G(u,v).

LaTeX

$$$$ G.Connected \Rightarrow \forall u,v, \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 (hconn : G.Connected) (u v : V) : ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v :=
  by
  obtain ⟨p, h⟩ := hconn.exists_walk_length_eq_dist u v
  exact ⟨p, p.isPath_of_length_eq_dist h, h⟩

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