tail_cons — Mathlib

English

If p is a walk from u to v and h is an adjacency from u to v, then the tail of p.cons h is the same as the tail of p (up to reindexing): (p.cons h).tail = p.copy (getVert_zero p).symm rfl.

Русский

Пусть p — ход от u к v, и h — смежность; хвост хода p cons h совпадает с хвостом p (с учётом переназначения первого вершины).

LaTeX

$$$ (p.cons\\ h).tail = p.copy (getVert_zero p).symm rfl $$$

Lean4

@[simp]
theorem tail_cons (h : G.Adj u v) (p : G.Walk v w) : (p.cons h).tail = p.copy (getVert_zero p).symm rfl := by
  match p with
  | .nil => rfl
  | .cons h q => rfl

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