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.

ink

class Denumerable (α : Type u_1) extends Encodable : Type u_1

• decode and encode are inverses.

  decode_inv : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n

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

ink

theorem Denumerable.decode_isSome (α : Type u_1) [inst : Denumerable α] (n : ℕ) : Option.isSome (Encodable.decode n) = true

ink

def Denumerable.ofNat (α : Type u_1) [inst : Denumerable α] (n : ℕ) : α

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

Equations

• Denumerable.ofNat α n = Option.get (Encodable.decode n) (_ : Option.isSome (Encodable.decode n) = true)

ink

@[simp]

theorem Denumerable.decode_eq_ofNat (α : Type u_1) [inst : Denumerable α] (n : ℕ) : Encodable.decode n = some (Denumerable.ofNat α n)

ink

@[simp]

theorem Denumerable.ofNat_of_decode {α : Type u_1} [inst : Denumerable α] {n : ℕ} {b : α} (h : Encodable.decode n = some b) : Denumerable.ofNat α n = b

ink

@[simp]

theorem Denumerable.encode_ofNat {α : Type u_1} [inst : Denumerable α] (n : ℕ) : Encodable.encode (Denumerable.ofNat α n) = n

ink

@[simp]

theorem Denumerable.ofNat_encode {α : Type u_1} [inst : Denumerable α] (a : α) : Denumerable.ofNat α (Encodable.encode a) = a

ink

def Denumerable.eqv (α : Type u_1) [inst : Denumerable α] : α ≃ ℕ

A denumerable type is equivalent to ℕ.

Equations

• One or more equations did not get rendered due to their size.

ink

instance Denumerable.instInfinite {α : Type u_1} [inst : Denumerable α] : Infinite α

Equations

• @Denumerable.instInfinite = @Denumerable.instInfinite.proof_1

ink

def Denumerable.mk' {α : Type u_1} (e : α ≃ ℕ) : Denumerable α

A type equivalent to ℕ is denumerable.

Equations

• Denumerable.mk' e = Denumerable.mk (_ : ∀ (x : ℕ), ∃ a, a ∈ Encodable.decode x ∧ Encodable.encode a = x)

ink

def Denumerable.ofEquiv (α : Type u_1) {β : Type u_2} [inst : Denumerable α] (e : β ≃ α) : Denumerable β

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

Equations

• Denumerable.ofEquiv α e = let src := Encodable.ofEquiv α e; Denumerable.mk (_ : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n)

ink

@[simp]

theorem Denumerable.ofEquiv_ofNat (α : Type u_1) {β : Type u_2} [inst : Denumerable α] (e : β ≃ α) (n : ℕ) : Denumerable.ofNat β n = ↑(Equiv.symm e) (Denumerable.ofNat α n)

ink

def Denumerable.equiv₂ (α : Type u_1) (β : Type u_2) [inst : Denumerable α] [inst : Denumerable β] : α ≃ β

All denumerable types are equivalent.

Equations

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

ink

instance Denumerable.nat : Denumerable ℕ

Equations

• Denumerable.nat = Denumerable.mk Denumerable.nat.proof_1

ink

@[simp]

theorem Denumerable.ofNat_nat (n : ℕ) : Denumerable.ofNat ℕ n = n

ink

instance Denumerable.option {α : Type u_1} [inst : Denumerable α] : Denumerable (Option α)

If α is denumerable, then so is option α.

Equations

• Denumerable.option = Denumerable.mk (_ : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n)

ink

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

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

Equations

• Denumerable.sum = Denumerable.mk (_ : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n)

ink

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

A denumerable collection of denumerable types is denumerable.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Denumerable.sigma_ofNat_val {α : Type u_1} [inst : Denumerable α] {γ : α → Type u_2} [inst : (a : α) → Denumerable (γ a)] (n : ℕ) : Denumerable.ofNat (Sigma γ) n = { fst := Denumerable.ofNat α (Nat.unpair n).fst, snd := Denumerable.ofNat (γ (Denumerable.ofNat α (Nat.unpair n).fst)) (Nat.unpair n).snd }

ink

instance Denumerable.prod {α : Type u_1} {β : Type u_2} [inst : Denumerable α] [inst : Denumerable β] : Denumerable (α × β)

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

Equations

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

ink

theorem Denumerable.prod_ofNat_val {α : Type u_1} {β : Type u_2} [inst : Denumerable α] [inst : Denumerable β] (n : ℕ) : Denumerable.ofNat (α × β) n = (Denumerable.ofNat α (Nat.unpair n).fst, Denumerable.ofNat β (Nat.unpair n).snd)

ink

@[simp]

theorem Denumerable.prod_nat_ofNat : Denumerable.ofNat (ℕ × ℕ) = Nat.unpair

ink

instance Denumerable.int : Denumerable ℤ

Equations

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

ink

instance Denumerable.pnat : Denumerable ℕ+

Equations

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

ink

instance Denumerable.ulift {α : Type u_1} [inst : Denumerable α] : Denumerable (ULift α)

The lift of a denumerable type is denumerable.

Equations

• Denumerable.ulift = Denumerable.ofEquiv α Equiv.ulift

ink

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

The lift of a denumerable type is denumerable.

Equations

• Denumerable.plift = Denumerable.ofEquiv α Equiv.plift

ink

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

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

Equations

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

Subsets of ℕ

ink

theorem Nat.Subtype.exists_succ {s : Set ℕ} [inst : Infinite ↑s] (x : ↑s) : ∃ n, ↑x + n + 1 ∈ s

ink

def Nat.Subtype.succ {s : Set ℕ} [inst : Infinite ↑s] [inst : 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 = let_fun h := (_ : ∃ n, ↑x + n + 1 ∈ s); { val := ↑x + Nat.find h + 1, property := (_ : ↑x + Nat.find h + 1 ∈ s) }

ink

theorem Nat.Subtype.succ_le_of_lt {s : Set ℕ} [inst : Infinite ↑s] [inst : DecidablePred fun x => x ∈ s] {x : ↑s} {y : ↑s} (h : y < x) : Nat.Subtype.succ y ≤ x

ink

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

ink

theorem Nat.Subtype.lt_succ_self {s : Set ℕ} [inst : Infinite ↑s] [inst : DecidablePred fun x => x ∈ s] (x : ↑s) : x < Nat.Subtype.succ x

ink

theorem Nat.Subtype.lt_succ_iff_le {s : Set ℕ} [inst : Infinite ↑s] [inst : DecidablePred fun x => x ∈ s] {x : ↑s} {y : ↑s} : x < Nat.Subtype.succ y ↔ x ≤ y

ink

def Nat.Subtype.ofNat (s : Set ℕ) [inst : DecidablePred fun x => x ∈ s] [inst : 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 (Nat.succ n) = Nat.Subtype.succ (Nat.Subtype.ofNat s n)

ink

theorem Nat.Subtype.ofNat_surjective_aux {s : Set ℕ} [inst : Infinite ↑s] [inst : DecidablePred fun x => x ∈ s] {x : ℕ} (hx : x ∈ s) : ∃ n, Nat.Subtype.ofNat s n = { val := x, property := hx }

ink

theorem Nat.Subtype.ofNat_surjective {s : Set ℕ} [inst : Infinite ↑s] [inst : DecidablePred fun x => x ∈ s] : Function.Surjective (Nat.Subtype.ofNat s)

ink

@[simp]

theorem Nat.Subtype.ofNat_range {s : Set ℕ} [inst : Infinite ↑s] [inst : DecidablePred fun x => x ∈ s] : Set.range (Nat.Subtype.ofNat s) = Set.univ

ink

@[simp]

theorem Nat.Subtype.coe_comp_ofNat_range {s : Set ℕ} [inst : Infinite ↑s] [inst : DecidablePred fun x => x ∈ s] : Set.range (Subtype.val ∘ Nat.Subtype.ofNat s) = s

ink

def Nat.Subtype.denumerable (s : Set ℕ) [inst : DecidablePred fun x => x ∈ s] [inst : Infinite ↑s] : Denumerable ↑s

Any infinite set of naturals is denumerable.

Equations

• One or more equations did not get rendered due to their size.

ink

def Denumerable.ofEncodableOfInfinite (α : Type u_1) [inst : Encodable α] [inst : Infinite α] : Denumerable α

An infinite encodable type is denumerable.

Equations

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

ink

theorem nonempty_denumerable (α : Type u_1) [inst : Countable α] [inst : Infinite α] : Nonempty (Denumerable α)

See also nonempty_encodable, nonempty_fintype.

ink

instance nonempty_equiv_of_countable {α : Type u_1} {β : Type u_2} [inst : Countable α] [inst : Infinite α] [inst : Countable β] [inst : Infinite β] : Nonempty (α ≃ β)

Equations

• @nonempty_equiv_of_countable = @nonempty_equiv_of_countable.proof_1