isPath_of_isSubwalk — Mathlib

English

If p1 is a subwalk of p2 and p2 is a path, then p1 is a path.

Русский

Если p1 является подпроходом p2, а p2 — путь, то p1 — путь.

LaTeX

$$$ p1.IsSubwalk(p2) \land p2.IsPath \Rightarrow p1.IsPath $$$

Lean4

theorem isPath_of_isSubwalk {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'} (h : p₁.IsSubwalk p₂)
    (h₂ : p₂.IsPath) : p₁.IsPath := by
  obtain ⟨_, _, h⟩ := h
  rw [h] at h₂
  exact h₂.of_append_left.of_append_right

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