get_tail_succ — Mathlib

English

For a vector v of length n+1, the tail’s i-th element equals the v's (i+1)-th element.

Русский

Для вектора длины n+1 хвостовой элемент i-й позиции равен (i+1)-му элементу вектора.

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,(n+1),\forall i:\mathrm{Fin}\,n,\ (\mathrm{tail}\;v)\ i = v\ i.succ$$$

Lean4

@[simp]
theorem get_tail_succ : ∀ (v : Vector α n.succ) (i : Fin n), get (tail v) i = get v i.succ
  | ⟨a :: l, e⟩, ⟨i, h⟩ => by simp [get_eq_get_toList]; rfl

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