isPath_of_length_eq_dist — Mathlib

English

If p is a walk from u to v and length(p) = dist_G(u,v), then p is a path.

Русский

Если ход p — обход от u к v и длина p равна dist_G(u,v), то p является путём.

LaTeX

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

Lean4

theorem isPath_of_length_eq_dist (p : G.Walk u v) (hp : p.length = G.dist u v) : p.IsPath := by
  classical
  have : p.bypass = p := by
    apply Walk.bypass_eq_self_of_length_le
    calc
      p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass
  rw [← this]
  apply Walk.bypass_isPath

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