getVert_copy — Mathlib

English

If p is a walk from u to v and h, h' are endpoint equalities, then copying p along h and h' preserves the vertex at position i: (p.copy h h').getVert i = p.getVert i.

Русский

Если ход p от u к v и заданы равенства концов, копирование p сохраняет вершину на позиции i: (p.copy h h').getVert i = p.getVert i.

LaTeX

$$$ (p.copy\\ h\\ h').getVert\\ i = p.getVert\\ i $$$

Lean4

@[simp]
theorem getVert_copy {u v w x : V} (p : G.Walk u v) (i : ℕ) (h : u = w) (h' : v = x) :
    (p.copy h h').getVert i = p.getVert i := by
  subst_vars
  rfl

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