last_def — Mathlib

English

The last element of a vector of length n+1 is equal to its get at Fin.last n.

Русский

Последний элемент вектора длины n+1 равен его get(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. -/
theorem last_def {v : Vector α (n + 1)} : v.last = v.get (Fin.last n) :=
  rfl

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