getVert_cons — Mathlib

English

If p is a walk from v to w and h is an edge from u to v, then for any n ≠ 0, the n-th vertex of the extended walk (p.cons h) is the (n−1)-st vertex of p.

Русский

Если p — путь от v к w и h — ребро от u к v, то для любого n ≠ 0 вершина (p.cons h) на позиции n равна вершине p на позиции (n−1).

LaTeX

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

Lean4

theorem getVert_cons {u v w n} (p : G.Walk v w) (h : G.Adj u v) (hn : n ≠ 0) :
    (p.cons h).getVert n = p.getVert (n - 1) :=
  by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
  rw [getVert_cons_succ, Nat.add_sub_cancel]

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