Documentation

Mathlib.Logic.Denumerable

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 Encodable :

Type u_3

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

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

Instances

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

∃ a ∈ Encodable.decode n, Encodable.encode a = n

decode and encode are inverses.

theorem Denumerable.decode_isSome (α : Type u_3) [Denumerable α] (n : ℕ) :

(Encodable.decode n).isSome = true

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 ⋯

@[simp]

theorem Denumerable.decode_eq_ofNat (α : Type u_3) [Denumerable α] (n : ℕ) :

Encodable.decode n = some (Denumerable.ofNat α n)

@[simp]

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

Denumerable.ofNat α n = b

@[simp]

theorem Denumerable.encode_ofNat {α : Type u_1} [Denumerable α] (n : ℕ) :

Encodable.encode (Denumerable.ofNat α n) = n

@[simp]

theorem Denumerable.ofNat_encode {α : Type u_1} [Denumerable α] (a : α) :

Denumerable.ofNat α (Encodable.encode a) = a

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 := ⋯ }

@[instance 100]

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

Equations

⋯ = ⋯

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

A type equivalent to ℕ is denumerable.

Equations

Denumerable.mk' e = Denumerable.mk ⋯

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

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

Equations

Denumerable.ofEquiv α e = Denumerable.mk ⋯

@[simp]

theorem Denumerable.ofEquiv_ofNat (α : Type u_3) {β : Type u_4} [Denumerable α] (e : β ≃ α) (n : ℕ) :

Denumerable.ofNat β n = e.symm (Denumerable.ofNat α n)

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

instance Denumerable.nat :

Denumerable ℕ

Equations

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

@[simp]

theorem Denumerable.ofNat_nat (n : ℕ) :

Denumerable.ofNat ℕ n = n

instance Denumerable.option {α : Type u_1} [Denumerable α] :

Denumerable (Option α)

If α is denumerable, then so is Option α.

Equations

Denumerable.option = Denumerable.mk ⋯

instance Denumerable.sum {α : Type u_1} {β : Type u_2} [Denumerable α] [Denumerable β] :

Denumerable (α ⊕ β)

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

Equations

Denumerable.sum = Denumerable.mk ⋯

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 = Denumerable.mk ⋯

@[simp]

theorem Denumerable.sigma_ofNat_val {α : Type u_1} [Denumerable α] {γ : α → Type u_3} [(a : α) → Denumerable (γ a)] (n : ℕ) :

Denumerable.ofNat (Sigma γ) n = ⟨Denumerable.ofNat α (Nat.unpair n).1, Denumerable.ofNat (γ (Denumerable.ofNat α (Nat.unpair n).1)) (Nat.unpair n).2⟩

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

theorem Denumerable.prod_ofNat_val {α : Type u_1} {β : Type u_2} [Denumerable α] [Denumerable β] (n : ℕ) :

Denumerable.ofNat (α × β) n = (Denumerable.ofNat α (Nat.unpair n).1, Denumerable.ofNat β (Nat.unpair n).2)

@[simp]

theorem Denumerable.prod_nat_ofNat :

Denumerable.ofNat (ℕ × ℕ) = Nat.unpair

instance Denumerable.int :

Denumerable ℤ

Equations

Denumerable.int = Denumerable.mk' Equiv.intEquivNat

instance Denumerable.pnat :

Denumerable ℕ+

Equations

Denumerable.pnat = Denumerable.mk' Equiv.pnatEquivNat

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

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

Denumerable (PLift α)

The lift of a denumerable type is denumerable.

Equations

Denumerable.plift = Denumerable.ofEquiv α Equiv.plift

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

α × α ≃ α

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

Equations

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

Subsets of `ℕ` #

theorem Nat.Subtype.exists_succ {s : Set ℕ} [Infinite ↑s] (x : ↑s) :

∃ (n : ℕ), ↑x + n + 1 ∈ s

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, ⋯⟩

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

Nat.Subtype.succ y ≤ x

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

x ≤ Nat.Subtype.succ y

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

x < Nat.Subtype.succ x

theorem Nat.Subtype.lt_succ_iff_le {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] {x : ↑s} {y : ↑s} :

x < Nat.Subtype.succ y ↔ x ≤ y

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)

@[irreducible]

theorem Nat.Subtype.ofNat_surjective_aux {s : Set ℕ} [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] {x : ℕ} (hx : x ∈ s) :

∃ (n : ℕ), Nat.Subtype.ofNat s n = ⟨x, hx⟩

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

Function.Surjective (Nat.Subtype.ofNat s)

@[simp]

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

Set.range (Nat.Subtype.ofNat s) = Set.univ

@[simp]

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

Set.range (Subtype.val ∘ Nat.Subtype.ofNat s) = s

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 := ⋯ }

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

An infinite encodable type is denumerable.

Equations

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

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

Nonempty (Denumerable α)

See also nonempty_encodable, nonempty_fintype.

theorem nonempty_denumerable_iff {α : Type u_3} :

Nonempty (Denumerable α) ↔ Countable α ∧ Infinite α

instance nonempty_equiv_of_countable {α : Type u_1} {β : Type u_2} [Countable α] [Infinite α] [Countable β] [Infinite β] :

Nonempty (α ≃ β)

Equations

⋯ = ⋯