isSubwalk_of_append_right — Mathlib

English

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

Русский

Если p3 = p1.append(p2), то p2 является подпрохождением к 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_2.IsSubwalk p_3.$$$

Lean4

theorem isSubwalk_of_append_right {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₃ :=
  ⟨p₁, nil, append_nil _ ▸ h⟩

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