get_cons_succ — Mathlib

English

For a vector formed as a ::ᵥ v and i : Fin n, the (i+1)-th element equals the i-th element of v.

Русский

Для вектора a ::ᵥ v и i : Fin n, элемент с индексом i.succ равен элементу i в v.

LaTeX

$$$\\forall {\\alpha} {n} (a:\\alpha) (v:\\mathrm{Vector}\\ \\alpha\\ n) (i:\\mathrm{Fin} n),\\; \\mathrm{get}(\\mathrm{cons}(a,v), i.succ) = \\mathrm{get}(v,i)$$$

Lean4

@[simp]
theorem get_cons_succ (a : α) (v : Vector α n) (i : Fin n) : get (a ::ᵥ v) i.succ = get v i := by
  rw [← get_tail_succ, tail_cons]

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