reverse_reverse

Mathlib.Data.Vector.Basic

URI: https://scilib.ai/kg/mathlib#List.Vector.reverse_reverse

English

The reverse of a vector, reversed again, yields the original vector.

Русский

Обратный к вектору, затем снова обращённый, даёт исходный вектор.

LaTeX

$$$\\forall \\alpha\\;\\forall n\\;\\forall v:\\mathrm{Vector}\\ \\alpha\\ n,\\; \\mathrm{reverse}(\\mathrm{reverse}(v)) = v$$$

Lean4

@[simp]
theorem reverse_reverse {v : Vector α n} : v.reverse.reverse = v :=
  by
  cases v
  simp [Vector.reverse]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru