mathlib documentation

data.equiv.list

source
def encodable.encode_list {α : Type u_1} [encodable α] (a : list α) :
ℕ

Equations
source
def encodable.decode_list {α : Type u_1} [encodable α] (a : ℕ) :
option (list α)

Equations
source
@[instance]
def encodable.list {α : Type u_1} [encodable α] :
encodable (list α)

Equations
source
@[simp]
theorem encodable.encode_list_nil {α : Type u_1} [encodable α] :
encodable.encode list.nil = 0

source
@[simp]
theorem encodable.encode_list_cons {α : Type u_1} [encodable α] (a : α) (l : list α) :
encodable.encode (a :: l) = ((encodable.encode a).mkpair (encodable.encode l)).succ

source
@[simp]
theorem encodable.decode_list_zero {α : Type u_1} [encodable α] :
encodable.decode (list α) 0 = some list.nil

source
@[simp]
theorem encodable.decode_list_succ {α : Type u_1} [encodable α] (v : ℕ) :
encodable.decode (list α) v.succ = (λ (_x : α) (_y : list α), _x :: _y) <$> encodable.decode α v.unpair.fst <*> encodable.decode (list α) v.unpair.snd

source
theorem encodable.length_le_encode {α : Type u_1} [encodable α] (l : list α) :
l.length ≤ encodable.encode l

source
def encodable.encode_multiset {α : Type u_1} [encodable α] (s : multiset α) :
ℕ

Equations
source
def encodable.decode_multiset {α : Type u_1} [encodable α] (n : ℕ) :
option (multiset α)

Equations
source
@[instance]
def encodable.multiset {α : Type u_1} [encodable α] :
encodable (multiset α)

Equations
source
def encodable.encodable_of_list {α : Type u_1} [decidable_eq α] (l : list α) (H : ∀ (x : α), x ∈ l) :
encodable α

Equations
source
def encodable.trunc_encodable_of_fintype (α : Type u_1) [decidable_eq α] [fintype α] :
trunc (encodable α)

Equations
source
@[instance]
def encodable.vector {α : Type u_1} [encodable α] {n : ℕ} :
encodable (vector α n)

Equations
source
@[instance]
def encodable.fin_arrow {α : Type u_1} [encodable α] {n : ℕ} :
encodable (fin n → α)

Equations
source
@[instance]
def encodable.fin_pi (n : ℕ) (π : fin n → Type u_1) [Π (i : fin n), encodable («π» i)] :
encodable (Π (i : fin n), «π» i)

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

Equations
source
@[instance]
def encodable.finset {α : Type u_1} [encodable α] :
encodable (finset α)

Equations
source
def encodable.fintype_arrow (α : Type u_1) (β : Type u_2) [decidable_eq α] [fintype α] [encodable β] :
trunc (encodable (α → β))

Equations
source
def encodable.fintype_pi (α : Type u_1) (π : α → Type u_2) [decidable_eq α] [fintype α] [Π (a : α), encodable («π» a)] :
trunc (encodable (Π (a : α), «π» a))

Equations
source
def encodable.sorted_univ (α : Type u_1) [fintype α] [encodable α] :
list α

The elements of a fintype as a sorted list.

Equations
source
theorem encodable.mem_sorted_univ {α : Type u_1} [fintype α] [encodable α] (x : α) :
x ∈ encodable.sorted_univ α

source
theorem encodable.length_sorted_univ {α : Type u_1} [fintype α] [encodable α] :
(encodable.sorted_univ α).length = fintype.card α

source
theorem encodable.sorted_univ_nodup {α : Type u_1} [fintype α] [encodable α] :
(encodable.sorted_univ α).nodup

source
def encodable.fintype_equiv_fin {α : Type u_1} [fintype α] [encodable α] :
α ≃ fin (fintype.card α)

An encodable fintype is equivalent a fin.

Equations
source
@[instance]
def encodable.fintype_arrow_of_encodable {α : Type u_1} {β : Type u_2} [encodable α] [fintype α] [encodable β] :
encodable (α → β)

Equations
source
theorem denumerable.denumerable_list_aux {α : Type u_1} [denumerable α] (n : ℕ) :
∃ (a : list α) (H : a ∈ encodable.decode_list n), encodable.encode_list a = n

source
@[instance]
def denumerable.denumerable_list {α : Type u_1} [denumerable α] :
denumerable (list α)

Equations
source
@[simp]
theorem denumerable.list_of_nat_zero {α : Type u_1} [denumerable α] :
denumerable.of_nat (list α) 0 = list.nil

source
@[simp]
theorem denumerable.list_of_nat_succ {α : Type u_1} [denumerable α] (v : ℕ) :
denumerable.of_nat (list α) v.succ = denumerable.of_nat α v.unpair.fst :: denumerable.of_nat (list α) v.unpair.snd

source
def denumerable.lower (a : list ℕ) (a_1 : ℕ) :
list ℕ

Equations
source
def denumerable.raise (a : list ℕ) (a_1 : ℕ) :
list ℕ

Equations
source
theorem denumerable.lower_raise (l : list ℕ) (n : ℕ) :
denumerable.lower (denumerable.raise l n) n = l

source
theorem denumerable.raise_lower {l : list ℕ} {n : ℕ} (a : list.sorted has_le.le (n :: l)) :
denumerable.raise (denumerable.lower l n) n = l

source
theorem denumerable.raise_chain (l : list ℕ) (n : ℕ) :
list.chain has_le.le n (denumerable.raise l n)

source
theorem denumerable.raise_sorted (l : list ℕ) (n : ℕ) :
list.sorted has_le.le (denumerable.raise l n)

source
@[instance]
def denumerable.multiset {α : Type u_1} [denumerable α] :
denumerable (multiset α)

Equations
source
def denumerable.lower' (a : list ℕ) (a_1 : ℕ) :
list ℕ

Equations
source
def denumerable.raise' (a : list ℕ) (a_1 : ℕ) :
list ℕ

Equations
source
theorem denumerable.lower_raise' (l : list ℕ) (n : ℕ) :
denumerable.lower' (denumerable.raise' l n) n = l

source
theorem denumerable.raise_lower' {l : list ℕ} {n : ℕ} (a : ∀ (m : ℕ), m ∈ l → n ≤ m) (a_1 : list.sorted has_lt.lt l) :
denumerable.raise' (denumerable.lower' l n) n = l

source
theorem denumerable.raise'_chain (l : list ℕ) {m n : ℕ} (a : m < n) :
list.chain has_lt.lt m (denumerable.raise' l n)

source
theorem denumerable.raise'_sorted (l : list ℕ) (n : ℕ) :
list.sorted has_lt.lt (denumerable.raise' l n)

source
def denumerable.raise'_finset (l : list ℕ) (n : ℕ) :
finset ℕ

Equations
source
@[instance]
def denumerable.finset {α : Type u_1} [denumerable α] :
denumerable (finset α)

Equations
source
def equiv.list_unit_equiv  :
list unit ≃ ℕ

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

Equations
source
def equiv.list_nat_equiv_nat  :
list ℕ ≃ ℕ

Equations
source
def equiv.list_equiv_self_of_equiv_nat {α : Type} (e : α ≃ ℕ) :
list α ≃ α

Equations