Equations
- encodable.encode_list (a :: l) = ((encodable.encode a).mkpair (encodable.encode_list l)).succ
- encodable.encode_list list.nil = 0
Equations
- encodable.decode_list v.succ = encodable.decode_list._match_1 v (λ (v₁ v₂ : ℕ) (h : (v₁, v₂).snd ≤ v) (this : v₂ < v.succ), encodable.decode_list v₂) v.unpair _
- encodable.decode_list 0 = some list.nil
- encodable.decode_list._match_1 v _f_1 (v₁, v₂) h = have this : v₂ < v.succ, from _, (λ (_x : α) (_y : list α), _x :: _y) <$> encodable.decode α v₁ <*> _f_1 v₁ v₂ h this
@[protected, instance]
Equations
- encodable.list = {encode := encodable.encode_list _inst_1, decode := encodable.decode_list _inst_1, encodek := _}
@[simp]
@[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
@[simp]
theorem
encodable.decode_list_zero
{α : Type u_1}
[encodable α] :
encodable.decode (list α) 0 = some list.nil
@[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
theorem
encodable.length_le_encode
{α : Type u_1}
[encodable α]
(l : list α) :
l.length ≤ encodable.encode l
Equations
- encodable.encode_multiset s = encodable.encode (multiset.sort enle s)
Equations
- encodable.decode_multiset n = coe <$> encodable.decode (list α) n
@[protected, instance]
Equations
- encodable.multiset = {encode := encodable.encode_multiset _inst_1, decode := encodable.decode_multiset _inst_1, encodek := _}
def
encodable.encodable_of_list
{α : Type u_1}
[decidable_eq α]
(l : list α)
(H : ∀ (x : α), x ∈ l) :
Equations
- encodable.encodable_of_list l H = {encode := λ (a : α), list.index_of a l, decode := l.nth, encodek := _}
Equations
- encodable.trunc_encodable_of_fintype α = quot.rec_on_subsingleton finset.univ.val (λ (l : list α) (H : ∀ (x : α), x ∈ quot.mk setoid.r l), trunc.mk (encodable.encodable_of_list l H)) finset.mem_univ
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.encodable.
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- encodable.fin_pi n «π» = encodable.of_equiv ↥{f : fin n → (Σ (i : fin n), «π» i) | ∀ (i : fin n), (f i).fst = i} (equiv.pi_equiv_subtype_sigma (fin n) «π»)
@[protected, instance]
Equations
- encodable.array = encodable.of_equiv (fin n → α) (equiv.array_equiv_fin n α)
@[protected, instance]
Equations
- encodable.finset = encodable.of_equiv {s // s.nodup} {to_fun := λ (_x : finset α), encodable.finset._match_1 _x, inv_fun := λ (_x : {s // s.nodup}), encodable.finset._match_2 _x, left_inv := _, right_inv := _}
- encodable.finset._match_1 {val := a, nodup := b} = ⟨a, b⟩
- encodable.finset._match_2 ⟨a, b⟩ = {val := a, nodup := b}
def
encodable.fintype_arrow
(α : Type u_1)
(β : Type u_2)
[decidable_eq α]
[fintype α]
[encodable β] :
Equations
- encodable.fintype_arrow α β = trunc.map (λ (f : α ≃ fin (fintype.card α)), encodable.of_equiv (fin (fintype.card α) → β) (f.arrow_congr (equiv.refl β))) (fintype.trunc_equiv_fin α)
def
encodable.fintype_pi
(α : Type u_1)
(π : α → Type u_2)
[decidable_eq α]
[fintype α]
[Π (a : α), encodable («π» a)] :
Equations
- encodable.fintype_pi α «π» = (encodable.trunc_encodable_of_fintype α).bind (λ (a : encodable α), (encodable.fintype_arrow α (Σ (a : α), «π» a)).bind (λ (f : encodable (α → (Σ (a : α), «π» a))), trunc.mk (encodable.of_equiv {a // a ∈ {f : α → (Σ (i : α), «π» i) | ∀ (i : α), (f i).fst = i}} (equiv.pi_equiv_subtype_sigma α «π»))))
The elements of a fintype as a sorted list.
Equations
An encodable fintype is equivalent a fin.
Equations
- encodable.fintype_equiv_fin = (fintype.equiv_fin_of_forall_mem_list encodable.mem_sorted_univ encodable.sorted_univ_nodup).trans (equiv.cast encodable.fintype_equiv_fin._proof_1)
@[protected, instance]
def
encodable.fintype_arrow_of_encodable
{α : Type u_1}
{β : Type u_2}
[encodable α]
[fintype α]
[encodable β] :
encodable (α → β)
Equations
theorem
denumerable.denumerable_list_aux
{α : Type u_1}
[denumerable α]
(n : ℕ) :
∃ (a : list α) (H : a ∈ encodable.decode_list n), encodable.encode_list a = n
@[protected, instance]
Equations
@[simp]
theorem
denumerable.list_of_nat_zero
{α : Type u_1}
[denumerable α] :
denumerable.of_nat (list α) 0 = list.nil
@[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
Equations
- denumerable.lower (m :: l) n = (m - n) :: denumerable.lower l m
- denumerable.lower list.nil n = list.nil
Equations
- denumerable.raise (m :: l) n = (m + n) :: denumerable.raise l (m + n)
- denumerable.raise list.nil n = list.nil
theorem
denumerable.lower_raise
(l : list ℕ)
(n : ℕ) :
denumerable.lower (denumerable.raise l n) n = l
theorem
denumerable.raise_lower
{l : list ℕ}
{n : ℕ} :
list.sorted has_le.le (n :: l) → denumerable.raise (denumerable.lower l n) n = l
theorem
denumerable.raise_chain
(l : list ℕ)
(n : ℕ) :
list.chain has_le.le n (denumerable.raise l n)
@[protected, instance]
Equations
- denumerable.multiset = denumerable.mk' {to_fun := λ (s : multiset α), encodable.encode (denumerable.lower (multiset.sort has_le.le (multiset.map encodable.encode s)) 0), inv_fun := λ (n : ℕ), multiset.map (denumerable.of_nat α) ↑(denumerable.raise (denumerable.of_nat (list ℕ) n) 0), left_inv := _, right_inv := _}
Equations
- denumerable.lower' (m :: l) n = (m - n) :: denumerable.lower' l (m + 1)
- denumerable.lower' list.nil n = list.nil
Equations
- denumerable.raise' (m :: l) n = (m + n) :: denumerable.raise' l (m + n + 1)
- denumerable.raise' list.nil n = list.nil
theorem
denumerable.lower_raise'
(l : list ℕ)
(n : ℕ) :
denumerable.lower' (denumerable.raise' l n) n = l
theorem
denumerable.raise_lower'
{l : list ℕ}
{n : ℕ} :
(∀ (m : ℕ), m ∈ l → n ≤ m) → list.sorted has_lt.lt l → denumerable.raise' (denumerable.lower' l n) n = l
theorem
denumerable.raise'_chain
(l : list ℕ)
{m n : ℕ} :
m < n → list.chain has_lt.lt m (denumerable.raise' l n)
Equations
- denumerable.raise'_finset l n = {val := ↑(denumerable.raise' l n), nodup := _}
@[protected, instance]
Equations
- denumerable.finset = denumerable.mk' {to_fun := λ (s : finset α), encodable.encode (denumerable.lower' (finset.sort has_le.le (finset.map (denumerable.eqv α).to_embedding s)) 0), inv_fun := λ (n : ℕ), finset.map (denumerable.eqv α).symm.to_embedding (denumerable.raise'_finset (denumerable.of_nat (list ℕ) n) 0), left_inv := _, right_inv := _}
The type lists on unit is canonically equivalent to the natural numbers.
Equations
- equiv.list_unit_equiv = {to_fun := list.length unit, inv_fun := list.repeat (), left_inv := equiv.list_unit_equiv._proof_1, right_inv := equiv.list_unit_equiv._proof_2}