reverse — Mathlib

English

The reverse operation on vectors reverses the underlying list of elements.

Русский

Операция переворота над вектором разворачивает элементы в обратном порядке.

LaTeX

$$$\mathrm{reverse}\ v = \langle\mathrm{toList}\ v\rvert\mathrm{reverse},\ \text{proof}\rangle$ and $\mathrm{toList}(\mathrm{reverse}\ v) = \mathrm{List}.reverse(\mathrm{toList}(v))$$$

Lean4

/-- Reverse a vector. -/
def reverse (v : Vector α n) : Vector α n :=
  ⟨v.toList.reverse, by simp⟩

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