getVert_cons_succ — Mathlib

English

If p is a walk from v to w and h is an edge from u to v, then prepending h to p shifts the vertex sequence by one: (p.cons h).getVert(n+1) = p.getVert(n).

Русский

Если p — путь от v до w, а h — ребро от u до v, то добавление h в начале p сдвигает последовательность вершин на один; (p.cons h).getVert(n+1) = p.getVert(n).

LaTeX

$$$$\forall {u,v,w} (p : G.Walk v w),\ (h : G.Adj u v),\ \forall n \in \mathbb{N},\ (p.cons h).getVert(n+1) = p.getVert(n).$$$$

Lean4

@[simp]
theorem getVert_cons_succ {u v w n} (p : G.Walk v w) (h : G.Adj u v) : (p.cons h).getVert (n + 1) = p.getVert n :=
  rfl

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