# Documentation

Mathlib.Logic.Equiv.List

# Equivalences involving List-like types #

This file defines some additional constructive equivalences using Encodable and the pairing function on ℕ.

def Encodable.encodeList {α : Type u_1} [inst : ] :
List α

Explicit encoding function for List α

Equations
def Encodable.decodeList {α : Type u_1} [inst : ] :
Option (List α)

Explicit decoding function for List α

Equations
• One or more equations did not get rendered due to their size.
instance List.encodable {α : Type u_1} [inst : ] :

If α is encodable, then so is List α. This uses the mkpair and unpair functions from Data.Nat.Pairing.

Equations
• List.encodable = { encode := Encodable.encodeList, decode := Encodable.decodeList, encodek := (_ : ∀ (l : List α), ) }
instance List.countable {α : Type u_1} [inst : ] :
Equations
@[simp]
theorem Encodable.encode_list_nil {α : Type u_1} [inst : ] :
@[simp]
theorem Encodable.encode_list_cons {α : Type u_1} [inst : ] (a : α) (l : List α) :
@[simp]
theorem Encodable.decode_list_zero {α : Type u_1} [inst : ] :
@[simp]
theorem Encodable.decode_list_succ {α : Type u_1} [inst : ] (v : ) :
= Seq.seq ((fun x x_1 => x :: x_1) <$> Encodable.decode ().fst) fun x => Encodable.decode ().snd theorem Encodable.length_le_encode {α : Type u_1} [inst : ] (l : List α) : def Encodable.encodeMultiset {α : Type u_1} [inst : ] (s : ) : Explicit encoding function for Multiset α Equations def Encodable.decodeMultiset {α : Type u_1} [inst : ] (n : ) : Explicit decoding function for Multiset α Equations • = Multiset.ofList <$>
instance Multiset.encodable {α : Type u_1} [inst : ] :

If α is encodable, then so is Multiset α.

Equations
• One or more equations did not get rendered due to their size.
instance Multiset.countable {α : Type u_1} [inst : ] :

If α is countable, then so is Multiset α.

Equations
def Encodable.encodableOfList {α : Type u_1} [inst : ] (l : List α) (H : ∀ (x : α), x l) :

A listable type with decidable equality is encodable.

Equations
• = { encode := fun a => , decode := , encodek := (_ : ∀ (x : α), List.get? l () = some x) }
def Fintype.truncEncodable (α : Type u_1) [inst : ] [inst : ] :

A finite type is encodable. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

Equations
• One or more equations did not get rendered due to their size.
noncomputable def Fintype.toEncodable (α : Type u_1) [inst : ] :

A noncomputable way to arbitrarily choose an ordering on a finite type. It is not made into a global instance, since it involves an arbitrary choice. This can be locally made into an instance with local attribute [instance] Fintype.toEncodable.

Equations
instance Vector.encodable {α : Type u_1} [inst : ] {n : } :

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

Equations
• Vector.encodable = Encodable.Subtype.encodable
instance Vector.countable {α : Type u_1} [inst : ] {n : } :

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

Equations
instance Encodable.finArrow {α : Type u_1} [inst : ] {n : } :
Encodable (Fin nα)

If α is encodable, then so is Fin n → α→ α.

Equations
instance Encodable.finPi (n : ) (π : Fin nType u_1) [inst : (i : Fin n) → Encodable (π i)] :
Encodable ((i : Fin n) → π i)
Equations
instance Finset.encodable {α : Type u_1} [inst : ] :

If α is encodable, then so is Finset α.

Equations
• One or more equations did not get rendered due to their size.
instance Finset.countable {α : Type u_1} [inst : ] :

If α is countable, then so is Finset α.

Equations
def Encodable.fintypeArrow (α : Type u_1) (β : Type u_2) [inst : ] [inst : ] [inst : ] :
Trunc (Encodable (αβ))

When α is finite and β is encodable, α → β→ β is encodable too. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

Equations
def Encodable.fintypePi (α : Type u_1) (π : αType u_2) [inst : ] [inst : ] [inst : (a : α) → Encodable (π a)] :
Trunc (Encodable ((a : α) → π a))

When α is finite and all π a are encodable, Π a, π a is encodable too. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

Equations
• One or more equations did not get rendered due to their size.
def Encodable.sortedUniv (α : Type u_1) [inst : ] [inst : ] :
List α

The elements of a Fintype as a sorted list.

Equations
@[simp]
theorem Encodable.mem_sortedUniv {α : Type u_1} [inst : ] [inst : ] (x : α) :
@[simp]
theorem Encodable.length_sortedUniv (α : Type u_1) [inst : ] [inst : ] :
@[simp]
theorem Encodable.sortedUniv_nodup (α : Type u_1) [inst : ] [inst : ] :
@[simp]
theorem Encodable.sortedUniv_toFinset (α : Type u_1) [inst : ] [inst : ] [inst : ] :
= Finset.univ
def Encodable.fintypeEquivFin {α : Type u_1} [inst : ] [inst : ] :
α Fin ()

An encodable Fintype is equivalent to the same size fin.

Equations
• One or more equations did not get rendered due to their size.
instance Encodable.fintypeArrowOfEncodable {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] :
Encodable (αβ)

If α and β are encodable and α is a fintype, then α → β→ β is encodable as well.

Equations
theorem Denumerable.denumerable_list_aux {α : Type u_1} [inst : ] (n : ) :
a,
instance Denumerable.denumerableList {α : Type u_1} [inst : ] :

If α is denumerable, then so is List α.

Equations
@[simp]
theorem Denumerable.list_ofNat_zero {α : Type u_1} [inst : ] :
= []
@[simp]
theorem Denumerable.list_ofNat_succ {α : Type u_1} [inst : ] (v : ) :
def Denumerable.lower :

Outputs the list of differences of the input list, that is lower [a₁, a₂, ...] n = [a₁ - n, a₂ - a₁, ...]

Equations
def Denumerable.raise :

Outputs the list of partial sums of the input list, that is raise [a₁, a₂, ...] n = [n + a₁, n + a₁ + a₂, ...]

Equations
theorem Denumerable.lower_raise (l : ) (n : ) :
= l
theorem Denumerable.raise_lower {l : } {n : } :
List.Sorted (fun x x_1 => x x_1) (n :: l) = l
theorem Denumerable.raise_chain (l : ) (n : ) :
List.Chain (fun x x_1 => x x_1) n ()
theorem Denumerable.raise_sorted (l : ) (n : ) :
List.Sorted (fun x x_1 => x x_1) ()

raise l n is an non-decreasing sequence.

instance Denumerable.multiset {α : Type u_1} [inst : ] :

If α is denumerable, then so is Multiset α. Warning: this is not the same encoding as used in Multiset.encodable.

Equations
• One or more equations did not get rendered due to their size.
def Denumerable.lower' :

Outputs the list of differences minus one of the input list, that is lower' [a₁, a₂, a₃, ...] n = [a₁ - n, a₂ - a₁ - 1, a₃ - a₂ - 1, ...].

Equations
def Denumerable.raise' :

Outputs the list of partial sums plus one of the input list, that is raise [a₁, a₂, a₃, ...] n = [n + a₁, n + a₁ + a₂ + 1, n + a₁ + a₂ + a₃ + 2, ...]. Adding one each time ensures the elements are distinct.

Equations
theorem Denumerable.lower_raise' (l : ) (n : ) :
= l
theorem Denumerable.raise_lower' {l : } {n : } :
(∀ (m : ), m ln m) → List.Sorted (fun x x_1 => x < x_1) l = l
theorem Denumerable.raise'_chain (l : ) {m : } {n : } :
m < nList.Chain (fun x x_1 => x < x_1) m ()
theorem Denumerable.raise'_sorted (l : ) (n : ) :
List.Sorted (fun x x_1 => x < x_1) ()

raise' l n is a strictly increasing sequence.

def Denumerable.raise'Finset (l : ) (n : ) :

Makes raise' l n into a finset. Elements are distinct thanks to raise'_sorted.

Equations
instance Denumerable.finset {α : Type u_1} [inst : ] :

If α is denumerable, then so is finset α. Warning: this is not the same encoding as used in finset.encodable.

Equations
• One or more equations did not get rendered due to their size.

The type lists on unit is canonically equivalent to the natural numbers.

Equations

List ℕ is equivalent to ℕ.

Equations
def Equiv.listEquivSelfOfEquivNat {α : Type} (e : α ) :
List α α

If α is equivalent to ℕ, then List α is equivalent to α.

Equations