mathlib3 documentation

logic.equiv.array

Equivalences involving array #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We keep this separate from the file containing list-like equivalences as those have no future in mathlib4.

source
def equiv.d_array_equiv_fin {n : ℕ} (α : fin n → Type u_1) :
d_array n α ≃ Π (i : fin n), α i

The natural equivalence between length-n heterogeneous arrays and dependent functions from fin n.

Equations
source
def equiv.array_equiv_fin (n : ℕ) (α : Type u_1) :
array n α ≃ (fin n → α)

The natural equivalence between length-n arrays and functions from fin n.

Equations
source
def equiv.vector_equiv_array (α : Type u_1) (n : ℕ) :
vector α n ≃ array n α

The natural equivalence between length-n vectors and length-n arrays.

Equations
source
@[protected, instance]
def array.traversable {n : ℕ} :
traversable (array n)
Equations
source
@[protected, instance]
def array.is_lawful_traversable {n : ℕ} :
is_lawful_traversable (array n)
Equations
source
@[protected, instance]
def array.encodable {α : Type u_1} [encodable α] {n : ℕ} :
encodable (array n α)

If α is encodable, then so is array n α.

Equations
source
@[protected, instance]
def array.countable {α : Type u_1} [countable α] {n : ℕ} :
countable (array n α)

If α is countable, then so is array n α.