isSubwalk_cons — Mathlib

English

Let G be a SimpleGraph. If p is a walk from u to v and w is adjacent to u, then the walk obtained by prepending the edge (w,u) to p is a subwalk of the extended walk, i.e. p is a subwalk of p.cons(h).

Русский

Пусть G — простой граф. Пусть p — обход from u до v, и пусть w смежен с u. Тогда обход, полученный добавлением в начало пути ребра (w,u), имеет p как подпуть; то есть p является подподходом к p.cons(h).

LaTeX

$$$\forall G\;\forall u,v,w\;\forall p\in G.Walk\,u\,v\;\forall h\in G.Adj\,w\,u:\ IsSubwalk(p, p.cons(h)).$$$

Lean4

@[simp]
theorem isSubwalk_cons {u v w} (p : G.Walk u v) (h : G.Adj w u) : p.IsSubwalk (p.cons h) :=
  (isSubwalk_rfl p).cons h

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