English
If p1 is a shortest walk from u to v (length equals dist(u,v)) and p2 is a subwalk from u′ to v′ of p1, then its length equals dist(u′,v′).
Русский
Если p1 — кратчайший ход от u к v (длина равна dist(u,v)), а p2 — подход от u′ к v′, являющийся подпроходом p1, то его длина равна dist(u′,v′).
LaTeX
$$$ \forall p_1 : G.Walk\, u v, \forall p_2 : G.Walk\, u' v',\; p_1.\mathrm{length} = \operatorname{dist}(u,v) \;\land\; p_2 \text{ IsSubwalk } p_1 \Rightarrow p_2.\mathrm{length} = \operatorname{dist}(u',v'). $$$
Lean4
theorem length_eq_dist_of_subwalk {u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h₁ : p₁.length = G.dist u v)
(h₂ : p₂.IsSubwalk p₁) : p₂.length = G.dist u' v' :=
by
refine (dist_le _).eq_of_not_lt' fun hh ↦ ?_
obtain ⟨ru, rv, h⟩ := h₂
obtain ⟨s, _⟩ := p₂.reachable.exists_path_of_dist
let r := ru.append s |>.append rv
have : p₁.length = ru.length + p₂.length + rv.length := by simp [h]
have : r.length = ru.length + s.length + rv.length := by simp [r]
have := dist_le r
cutsat
