subset_support_append_left — Mathlib

English

For any walk p from u to v and q from v to w, the support of p is contained in the support of p.concat q.

Русский

Для обхода p: u→v и q: v→w, p.support ⊆ (p.append q).support.

LaTeX

$$$p.\mathrm{support} \subseteq (p.\mathrm{append}\ q).\mathrm{support}$$$

Lean4

@[simp]
theorem subset_support_append_left {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) :
    p.support ⊆ (p.append q).support := by simp only [Walk.support_append, List.subset_append_left]

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