arrayEquivList — Mathlib

English

There is a natural equivalence between arrays and lists given by converting an array to a list and back.

Русский

Существует естественное эквивалентное отображение между массивами и списками, задаваемое преобразованием массива в список и обратно.

LaTeX

$$$ \\text{Array }\\alpha \\simeq \\text{List }\\alpha $ via $\\text{toList}$ and $\\text{mk}$. $$

Lean4

/-- The natural equivalence between arrays and lists. -/
def arrayEquivList (α : Type*) : Array α ≃ List α
    where
  toFun := Array.toList
  invFun := Array.mk

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