# 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} [] :
List α

Explicit encoding function for List α

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

Explicit decoding function for List α

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

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

instance List.countable {α : Type u_2} [] :
@[simp]
theorem Encodable.encode_list_nil {α : Type u_1} [] :
@[simp]
theorem Encodable.encode_list_cons {α : Type u_1} [] (a : α) (l : List α) :
@[simp]
theorem Encodable.decode_list_zero {α : Type u_1} [] :
@[simp]
theorem Encodable.decode_list_succ {α : Type u_1} [] (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} [] (l : List α) :
def Encodable.encodeMultiset {α : Type u_1} [] (s : ) :

Explicit encoding function for Multiset α

Instances For
def Encodable.decodeMultiset {α : Type u_1} [] (n : ) :

Explicit decoding function for Multiset α

Instances For
instance Multiset.encodable {α : Type u_1} [] :

If α is encodable, then so is Multiset α.

instance Multiset.countable {α : Type u_2} [] :

If α is countable, then so is Multiset α.

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

A listable type with decidable equality is encodable.

Instances For
def Fintype.truncEncodable (α : Type u_2) [] [] :

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

Instances For
noncomputable def Fintype.toEncodable (α : Type u_2) [] :

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.

Instances For
instance Vector.encodable {α : Type u_1} [] {n : } :

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

instance Vector.countable {α : Type u_1} [] {n : } :

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

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

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

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

If α is encodable, then so is Finset α.

instance Finset.countable {α : Type u_1} [] :

If α is countable, then so is Finset α.

def Encodable.fintypeArrow (α : Type u_2) (β : Type u_3) [] [] [] :
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.

Instances For
def Encodable.fintypePi (α : Type u_2) (π : αType u_3) [] [] [(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.

Instances For
def Encodable.sortedUniv (α : Type u_2) [] [] :
List α

The elements of a Fintype as a sorted list.

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

An encodable Fintype is equivalent to the same size Fin.

Instances For
instance Encodable.fintypeArrowOfEncodable {α : Type u_2} {β : Type u_3} [] [] [] :
Encodable (αβ)

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

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

If α is denumerable, then so is List α.

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

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

Equations
Instances For
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
Instances For
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 a non-decreasing sequence.

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

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

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
Instances For
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
Instances For
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.

Instances For
instance Denumerable.finset {α : Type u_1} [] :

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

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

Instances For

List ℕ is equivalent to ℕ.

Instances For
def Equiv.listEquivSelfOfEquivNat {α : Type u_1} (e : α ) :
List α α

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

Instances For