toList — Mathlib

English

The operation toList converts a vector into the underlying list by taking the first component of the pair representing the vector.

Русский

Операция toList преобразует вектор в соответствующий ему список, извлекая первую компоненту пары, представляющей вектор.

LaTeX

$$$\\mathrm{toList}(\\langle l, h \\rangle) = l$$$

Lean4

/-- The list obtained from a vector. -/
def toList (v : Vector α n) : List α :=
  v.1

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