getVert_tail — Mathlib

English

For any p : G.Walk u v and n ∈ ℕ, the nth vertex of the tail equals the vertex at position n+1 of p: p.tail.getVert n = p.getVert (n+1).

Русский

Для хода p и любого n верщина хвоста на позиции n равна вершине на позиции n+1 в p: p.tail.getVert n = p.getVert (n+1).

LaTeX

$$$ p.tail.getVert n = p.getVert (n + 1) $$$

Lean4

@[simp]
theorem getVert_tail {u v n} (p : G.Walk u v) : p.tail.getVert n = p.getVert (n + 1) := by
  match p with
  | .nil => rfl
  | .cons h q =>
    simp only [getVert_cons_succ, tail_cons]
    exact getVert_copy q n (getVert_zero q).symm rfl

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