support_subset_support_concat — Mathlib

English

If p is a walk from u to v and hadj is an edge from v to w, then p.support is included in (p.concat hadj).support.

Русский

Если p — обход из u в v, а hadj — ребро v–w, то p.support ⊆ (p.concat hadj).support.

LaTeX

$$$p.\mathrm{support} \subseteq (p.\mathrm{concat}\ hadj).\mathrm{support}$$$

Lean4

theorem support_subset_support_concat {u v w : V} (p : G.Walk u v) (hadj : G.Adj v w) :
    p.support ⊆ (p.concat hadj).support := by simp

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