isSubwalk_of_append_left — Mathlib

English

If p3 equals p1 appended with p2, then p1 is a subwalk of p3.

Русский

Если p3 = p1.append(p2), то p1 является подпрохождением к p3.

LaTeX

$$$\forall v,w,u:\;{p_1:G.Walk\,v\,w},\ {p_2:G.Walk\,w\,u},\ {p_3:G.Walk\,v\,u},\ (p_3= p_1.append p_2)\Rightarrow p_1.IsSubwalk p_3.$$$

Lean4

theorem isSubwalk_of_append_left {v w u : V} {p₁ : G.Walk v w} {p₂ : G.Walk w u} {p₃ : G.Walk v u}
    (h : p₃ = p₁.append p₂) : p₁.IsSubwalk p₃ :=
  ⟨nil, p₂, h⟩

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