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.

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
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
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
@[protected, instance]
Equations
@[protected, instance]
def array.encodable {α : Type u_1} [encodable α] {n : } :

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

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

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