isTrail_of_isSubwalk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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