drop_getVert — Mathlib

English

The vertex obtained by getVert after dropping n steps equals the vertex obtained by getVert of the original walk at position n+m.

Русский

Вершина, полученная после сдвига на n шагов, равна вершине исходного хода на позиции n+m.

LaTeX

$$$ (p.drop n).getVert m = p.getVert (n + m) $$$

Lean4

@[simp]
theorem drop_getVert (p : G.Walk u v) (n m : ℕ) : (p.drop n).getVert m = p.getVert (n + m) := by
  induction p generalizing n with
  | nil => simp [drop]
  | cons => cases n <;> simp_all [drop, Nat.add_right_comm]

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