English
The head of the reverse of a vector is equal to the last element of the original vector.
Русский
Голова reverse(v) равна последнему элементу вектора v.
LaTeX
$$$\\forall {\\alpha} {n} (v:\\mathrm{Vector}\\ \\alpha\\ (n+1)),\\; v\\mathrm{.reverse}.head = v.last$$$
Lean4
/-- The `last` element of a vector is the `head` of the `reverse` vector. -/
theorem reverse_get_zero {v : Vector α (n + 1)} : v.reverse.head = v.last :=
by
rw [← get_zero, last_def, get_eq_get_toList, get_eq_get_toList]
simp_rw [toList_reverse]
rw [List.get_eq_getElem, List.get_eq_getElem, ← Option.some_inj, Fin.cast, Fin.cast, ← List.getElem?_eq_getElem, ←
List.getElem?_eq_getElem, List.getElem?_reverse]
· congr
simp
· simp
