get_tail — Mathlib

English

The i-th element of x.tail equals the (i+1)-th element of x.

Русский

i-й элемент x.tail равен (i+1)-му элементу x.

LaTeX

$$$\forall x:\mathrm{Vector}\,\alpha\,n,\ \forall i:\mathrm{Fin}\,(n),\ (x.tail).get\ i = x.get\langle i.1+1,\ \text{proof}\rangle$$$

Lean4

theorem get_tail (x : Vector α n) (i) : x.tail.get i = x.get ⟨i.1 + 1, by cutsat⟩ :=
  by
  obtain ⟨i, ih⟩ := i; dsimp
  rcases x with ⟨_ | _, h⟩ <;> try rfl
  rw [List.length] at h
  rw [← h] at ih
  contradiction

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