# 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.

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

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

- encode : α → ℕ
- decode : ℕ → Option α
- encodek (a : α) : decode (encode a) = some a
- decode_inv (n : ℕ) : ∃ a ∈ Encodable.decode n, Encodable.encode a = n

  `decode` and `encode` are inverses.

Instances

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

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

Equations

- Denumerable.ofNat α n = (Encodable.decode n).get ⋯

Instances For

source
@[simp]
theorem Denumerable.decode_eq_ofNat (α : Type u_3) [Denumerable α] (n : ℕ) :
Encodable.decode n = some (ofNat α n)
source
theorem Denumerable.ofNat_of_decode {α : Type u_1} [Denumerable α] {n : ℕ} {b : α} (h : Encodable.decode n = some b) :
ofNat α n = b
source
@[simp]
theorem Denumerable.encode_ofNat {α : Type u_1} [Denumerable α] (n : ℕ) :
Encodable.encode (ofNat α n) = n
source
@[simp]
theorem Denumerable.ofNat_encode {α : Type u_1} [Denumerable α] (a : α) :
ofNat α (Encodable.encode a) = a
source
def Denumerable.eqv (α : Type u_3) [Denumerable α] :
α ≃ ℕ

A denumerable type is equivalent to `ℕ`.

Equations

- Denumerable.eqv α = { toFun := Encodable.encode, invFun := Denumerable.ofNat α, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[instance 100]
instance Denumerable.instInfinite {α : Type u_1} [Denumerable α] :
Infinite α
source
def Denumerable.mk' {α : Type u_3} (e : α ≃ ℕ) :
Denumerable α

A type equivalent to `ℕ` is denumerable.

Equations

- Denumerable.mk' e = { encode := ⇑e, decode := some ∘ ⇑e.symm, encodek := ⋯, decode_inv := ⋯ }

Instances For

source
def Denumerable.ofEquiv (α : Type u_3) {β : Type u_4} [Denumerable α] (e : β ≃ α) :
Denumerable β

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

Equations

- Denumerable.ofEquiv α e = { toEncodable := Encodable.ofEquiv α e, decode_inv := ⋯ }

Instances For

source
@[simp]
theorem Denumerable.ofEquiv_ofNat (α : Type u_3) {β : Type u_4} [Denumerable α] (e : β ≃ α) (n : ℕ) :
ofNat β n = e.symm (ofNat α n)
source
def Denumerable.equiv₂ (α : Type u_3) (β : Type u_4) [Denumerable α] [Denumerable β] :
α ≃ β

All denumerable types are equivalent.

Equations

- Denumerable.equiv₂ α β = (Denumerable.eqv α).trans (Denumerable.eqv β).symm

Instances For

source
instance Denumerable.nat :
Denumerable ℕ
Equations

- Denumerable.nat = { toEncodable := Nat.encodable, decode_inv := Denumerable.nat._proof_1 }

source
@[simp]
theorem Denumerable.ofNat_nat (n : ℕ) :
ofNat ℕ n = n
source
instance Denumerable.option {α : Type u_1} [Denumerable α] :
Denumerable (Option α)

If `α` is denumerable, then so is `Option α`.

Equations

- Denumerable.option = { toEncodable := Option.encodable, decode_inv := ⋯ }

source
instance Denumerable.sum {α : Type u_1} {β : Type u_2} [Denumerable α] [Denumerable β] :
Denumerable (α ⊕ β)

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

Equations

- Denumerable.sum = { toEncodable := Sum.encodable, decode_inv := ⋯ }

source
instance Denumerable.sigma {α : Type u_1} [Denumerable α] {γ : α → Type u_3} [(a : α) → Denumerable (γ a)] :
Denumerable (Sigma γ)

A denumerable collection of denumerable types is denumerable.

Equations

- Denumerable.sigma = { toEncodable := Sigma.encodable, decode_inv := ⋯ }

source
@[simp]
theorem Denumerable.sigma_ofNat_val {α : Type u_1} [Denumerable α] {γ : α → Type u_3} [(a : α) → Denumerable (γ a)] (n : ℕ) :
ofNat (Sigma γ) n = ⟨ofNat α (Nat.unpair n).1, ofNat (γ (ofNat α (Nat.unpair n).1)) (Nat.unpair n).2⟩
source
instance Denumerable.prod {α : Type u_1} {β : Type u_2} [Denumerable α] [Denumerable β] :
Denumerable (α × β)

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

Equations

- Denumerable.prod = Denumerable.ofEquiv ((_ : α) × β) (Equiv.sigmaEquivProd α β).symm

source
theorem Denumerable.prod_ofNat_val {α : Type u_1} {β : Type u_2} [Denumerable α] [Denumerable β] (n : ℕ) :
ofNat (α × β) n = (ofNat α (Nat.unpair n).1, ofNat β (Nat.unpair n).2)
source
@[simp]
theorem Denumerable.prod_nat_ofNat :
ofNat (ℕ × ℕ) = Nat.unpair
source
instance Denumerable.int :
Denumerable ℤ
Equations

- Denumerable.int = Denumerable.mk' Equiv.intEquivNat

source
instance Denumerable.pnat :
Denumerable ℕ+
Equations

- Denumerable.pnat = Denumerable.mk' Equiv.pnatEquivNat

source
instance Denumerable.ulift {α : Type u_1} [Denumerable α] :
Denumerable (ULift.{u_3, u_1} α)

The lift of a denumerable type is denumerable.

Equations

- Denumerable.ulift = Denumerable.ofEquiv α Equiv.ulift

source
instance Denumerable.plift {α : Type u_1} [Denumerable α] :
Denumerable (PLift α)

The lift of a denumerable type is denumerable.

Equations

- Denumerable.plift = Denumerable.ofEquiv α Equiv.plift

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

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

Equations

- Denumerable.pair = Denumerable.equiv₂ (α × α) α

Instances For

### Subsets of `ℕ` #

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

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

Equations

- Nat.Subtype.succ x = ⟨↑x + Nat.find ⋯ + 1, ⋯⟩

Instances For

source
theorem Nat.Subtype.succ_le_of_lt {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] {x y : ↑s} (h : y < x) :
succ y ≤ x
source
theorem Nat.Subtype.le_succ_of_forall_lt_le {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] {x y : ↑s} (h : ∀ z < x, z ≤ y) :
x ≤ succ y
source
theorem Nat.Subtype.lt_succ_self {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] (x : ↑s) :
x < succ x
source
theorem Nat.Subtype.lt_succ_iff_le {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] {x y : ↑s} :
x < succ y ↔ x ≤ y
source
def Nat.Subtype.ofNat (s : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ s] [Infinite ↑s] :
ℕ → ↑s

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

Equations

- Nat.Subtype.ofNat s 0 = ⊥
- Nat.Subtype.ofNat s n.succ = Nat.Subtype.succ (Nat.Subtype.ofNat s n)

Instances For

source
@[irreducible]
theorem Nat.Subtype.ofNat_surjective {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] :
Function.Surjective (ofNat s)
source
@[simp]
theorem Nat.Subtype.ofNat_range {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] :
Set.range (ofNat s) = Set.univ
source
@[simp]
theorem Nat.Subtype.coe_comp_ofNat_range {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] :
Set.range (Subtype.val ∘ ofNat s) = s
source
def Nat.Subtype.denumerable (s : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ s] [Infinite ↑s] :
Denumerable ↑s

Any infinite set of naturals is denumerable.

Equations

- Nat.Subtype.denumerable s = Denumerable.ofEquiv ℕ { toFun := Nat.Subtype.toFunAux✝, invFun := Nat.Subtype.ofNat s, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
def Denumerable.ofEncodableOfInfinite (α : Type u_3) [Encodable α] [Infinite α] :
Denumerable α

An infinite encodable type is denumerable.

Equations

- Denumerable.ofEncodableOfInfinite α = Denumerable.ofEquiv (↑(Set.range Encodable.encode)) (Encodable.equivRangeEncode α)

Instances For

source
theorem nonempty_denumerable (α : Type u_3) [Countable α] [Infinite α] :
Nonempty (Denumerable α)

See also `nonempty_encodable`, `nonempty_fintype`.

source
theorem nonempty_denumerable_iff {α : Type u_3} :
Nonempty (Denumerable α) ↔ Countable α ∧ Infinite α
source
instance nonempty_equiv_of_countable {α : Type u_1} {β : Type u_2} [Countable α] [Infinite α] [Countable β] [Infinite β] :
Nonempty (α ≃ β)