last — Mathlib

English

The last element of a vector of length n+1 is obtained by getting the element at Fin.last n.

Русский

Последний элемент вектора длины n+1 равен элементу с индексом Fin.last n.

LaTeX

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

Lean4

/-- The last element of a `Vector`, given that the vector is at least one element. -/
def last (v : Vector α (n + 1)) : α :=
  v.get (Fin.last n)

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