length_le_of_isSubwalk — Mathlib

English

If p is a subwalk of q, then the length of p is at most the length of q.

Русский

Если p является подпрохождением к q, то длина p не больше длины q.

LaTeX

$$$\forall G\;\forall p,q:G.Walk\,\_,\ (IsSubwalk(p,q)\Rightarrow length(p)\le length(q)).$$$

Lean4

theorem length_le_of_isSubwalk {u₁ v₁ u₂ v₂} {q : G.Walk u₁ v₁} {p : G.Walk u₂ v₂} (h : p.IsSubwalk q) :
    p.length ≤ q.length := by grind [IsSubwalk, length_append]

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