Denumerable types #

This file defines denumerable (countably infinite) types as a typeclass extending Encodable. This is used to provide explicit encode/decode functions from and to ℕ, with the information that those functions are inverses of each other.

Implementation notes #

This property already has a name, namely α ≃ ℕ, but here we are interested in using it as a typeclass.

class Denumerable (α : Type u_3) extends :
Type u_3

A denumerable type is (constructively) bijective with ℕ. Typeclass equivalent of α ≃ ℕ.

• encode : α
• decode :
• encodek : ∀ (a : α),
• decode_inv : ∀ (n : ), a ∈ ,

decode and encode are inverses.

Instances
theorem Denumerable.decode_inv {α : Type u_3} [self : ] (n : ) :
a,

decode and encode are inverses.

theorem Denumerable.decode_isSome (α : Type u_3) [] (n : ) :
().isSome = true
def Denumerable.ofNat (α : Type u_3) [] (n : ) :
α

Returns the n-th element of α indexed by the decoding.

Equations
• = ().get
Instances For
@[simp]
theorem Denumerable.decode_eq_ofNat (α : Type u_3) [] (n : ) :
@[simp]
theorem Denumerable.ofNat_of_decode {α : Type u_1} [] {n : } {b : α} (h : ) :
= b
@[simp]
theorem Denumerable.encode_ofNat {α : Type u_1} [] (n : ) :
@[simp]
theorem Denumerable.ofNat_encode {α : Type u_1} [] (a : α) :
def Denumerable.eqv (α : Type u_3) [] :
α

A denumerable type is equivalent to ℕ.

Equations
• = { toFun := Encodable.encode, invFun := , left_inv := , right_inv := }
Instances For
@[instance 100]
instance Denumerable.instInfinite {α : Type u_1} [] :
Equations
• =
def Denumerable.mk' {α : Type u_3} (e : α ) :

A type equivalent to ℕ is denumerable.

Equations
Instances For
def Denumerable.ofEquiv (α : Type u_3) {β : Type u_4} [] (e : β α) :

Denumerability is conserved by equivalences. This is transitivity of equivalence the denumerable way.

Equations
• = let __src := ;
Instances For
@[simp]
theorem Denumerable.ofEquiv_ofNat (α : Type u_3) {β : Type u_4} [] (e : β α) (n : ) :
= e.symm ()
def Denumerable.equiv₂ (α : Type u_3) (β : Type u_4) [] [] :
α β

All denumerable types are equivalent.

Equations
• = ().trans ().symm
Instances For
instance Denumerable.nat :
Equations
@[simp]
theorem Denumerable.ofNat_nat (n : ) :
instance Denumerable.option {α : Type u_1} [] :

If α is denumerable, then so is Option α.

Equations
• Denumerable.option =
instance Denumerable.sum {α : Type u_1} {β : Type u_2} [] [] :

If α and β are denumerable, then so is their sum.

Equations
• Denumerable.sum =
instance Denumerable.sigma {α : Type u_1} [] {γ : αType u_3} [(a : α) → Denumerable (γ a)] :

A denumerable collection of denumerable types is denumerable.

Equations
• Denumerable.sigma =
@[simp]
theorem Denumerable.sigma_ofNat_val {α : Type u_1} [] {γ : αType u_3} [(a : α) → Denumerable (γ a)] (n : ) :
= Denumerable.ofNat α n.unpair.1, Denumerable.ofNat (γ (Denumerable.ofNat α n.unpair.1)) n.unpair.2
instance Denumerable.prod {α : Type u_1} {β : Type u_2} [] [] :
Denumerable (α × β)

If α and β are denumerable, then so is their product.

Equations
theorem Denumerable.prod_ofNat_val {α : Type u_1} {β : Type u_2} [] [] (n : ) :
Denumerable.ofNat (α × β) n = (Denumerable.ofNat α n.unpair.1, Denumerable.ofNat β n.unpair.2)
instance Denumerable.int :
Equations
instance Denumerable.pnat :
Equations
instance Denumerable.ulift {α : Type u_1} [] :

The lift of a denumerable type is denumerable.

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

The lift of a denumerable type is denumerable.

Equations
def Denumerable.pair {α : Type u_1} [] :
α × α α

If α is denumerable, then α × α and α are equivalent.

Equations
Instances For

Subsets of ℕ#

theorem Nat.Subtype.exists_succ {s : } [Infinite s] (x : s) :
∃ (n : ), x + n + 1 s
def Nat.Subtype.succ {s : } [Infinite s] [DecidablePred fun (x : ) => x s] (x : s) :
s

Returns the next natural in a set, according to the usual ordering of ℕ.

Equations
• = let_fun h := ; x + + 1,
Instances For
theorem Nat.Subtype.succ_le_of_lt {s : } [Infinite s] [DecidablePred fun (x : ) => x s] {x : s} {y : s} (h : y < x) :
theorem Nat.Subtype.le_succ_of_forall_lt_le {s : } [Infinite s] [DecidablePred fun (x : ) => x s] {x : s} {y : s} (h : z < x, z y) :
theorem Nat.Subtype.lt_succ_self {s : } [Infinite s] [DecidablePred fun (x : ) => x s] (x : s) :
theorem Nat.Subtype.lt_succ_iff_le {s : } [Infinite s] [DecidablePred fun (x : ) => x s] {x : s} {y : s} :
x y
def Nat.Subtype.ofNat (s : ) [DecidablePred fun (x : ) => x s] [Infinite s] :
s

Returns the n-th element of a set, according to the usual ordering of ℕ.

Equations
Instances For
theorem Nat.Subtype.ofNat_surjective_aux {s : } [Infinite s] [DecidablePred fun (x : ) => x s] {x : } (hx : x s) :
∃ (n : ), = x, hx
theorem Nat.Subtype.ofNat_surjective {s : } [Infinite s] [DecidablePred fun (x : ) => x s] :
@[simp]
theorem Nat.Subtype.ofNat_range {s : } [Infinite s] [DecidablePred fun (x : ) => x s] :
= Set.univ
@[simp]
theorem Nat.Subtype.coe_comp_ofNat_range {s : } [Infinite s] [DecidablePred fun (x : ) => x s] :
Set.range (Subtype.val ) = s
def Nat.Subtype.denumerable (s : ) [DecidablePred fun (x : ) => x s] [Infinite s] :

Any infinite set of naturals is denumerable.

Equations
Instances For

An infinite encodable type is denumerable.

Equations
Instances For
theorem nonempty_denumerable (α : Type u_3) [] [] :

See also nonempty_encodable, nonempty_fintype.

instance nonempty_equiv_of_countable {α : Type u_1} {β : Type u_2} [] [] [] [] :
Nonempty (α β)
Equations
• =