English
Let v be a vector of length n with elements in α. Then the list obtained by converting the reverse of v to a list is equal to the reverse of the list obtained from v.
Русский
Пусть v — вектор длины n над множеством α. Тогда список, полученный путём преобразования вектора после обращения к нему, равен обращённому списку самого вектора: toList(reverse(v)) = reverse(toList(v)).
LaTeX
$$$\\forall \\alpha\\;\\forall n\\;\\forall v:\\mathrm{Vector}\\ \\alpha\\ n,\\; \\mathrm{toList}(\\mathrm{reverse}(v)) = \\mathrm{reverse}(\\mathrm{toList}(v))$$$
Lean4
/-- The `List` of a vector after a `reverse`, retrieved by `toList` is equal
to the `List.reverse` after retrieving a vector's `toList`. -/
theorem toList_reverse {v : Vector α n} : v.reverse.toList = v.toList.reverse :=
rfl
