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_1) extends Encodable :
Type u_1

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

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

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

    Equations
    @[simp]
    @[simp]
    theorem Denumerable.ofNat_of_decode {α : Type u_1} [inst : Denumerable α] {n : } {b : α} (h : Encodable.decode n = some b) :
    @[simp]
    theorem Denumerable.encode_ofNat {α : Type u_1} [inst : Denumerable α] (n : ) :
    @[simp]
    theorem Denumerable.ofNat_encode {α : Type u_1} [inst : Denumerable α] (a : α) :
    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.
    def Denumerable.mk' {α : Type u_1} (e : α ) :

    A type equivalent to is denumerable.

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

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

    Equations
    @[simp]
    theorem Denumerable.ofEquiv_ofNat (α : Type u_1) {β : Type u_2} [inst : Denumerable α] (e : β α) (n : ) :
    def Denumerable.equiv₂ (α : Type u_1) (β : Type u_2) [inst : Denumerable α] [inst : Denumerable β] :
    α β

    All denumerable types are equivalent.

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

    If α is denumerable, then so is option α.

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

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

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

    A denumerable collection of denumerable types is denumerable.

    Equations
    • One or more equations did not get rendered due to their size.
    @[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 }
    instance Denumerable.prod {α : Type u_1} {β : Type u_2} [inst : Denumerable α] [inst : Denumerable β] :
    Denumerable (α × β)

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

    Equations
    theorem Denumerable.prod_ofNat_val {α : Type u_1} {β : Type u_2} [inst : Denumerable α] [inst : Denumerable β] (n : ) :
    instance Denumerable.ulift {α : Type u_1} [inst : Denumerable α] :

    The lift of a denumerable type is denumerable.

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

    The lift of a denumerable type is denumerable.

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

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

    Equations

    Subsets of #

    theorem Nat.Subtype.exists_succ {s : Set } [inst : Infinite s] (x : s) :
    n, x + n + 1 s
    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
    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) :
    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 < xz y) :
    theorem Nat.Subtype.lt_succ_self {s : Set } [inst : Infinite s] [inst : DecidablePred fun x => x s] (x : s) :
    theorem Nat.Subtype.lt_succ_iff_le {s : Set } [inst : Infinite s] [inst : DecidablePred fun x => x s] {x : s} {y : s} :
    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
    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 }
    @[simp]
    theorem Nat.Subtype.ofNat_range {s : Set } [inst : Infinite s] [inst : DecidablePred fun x => x s] :
    @[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
    def Nat.Subtype.denumerable (s : Set ) [inst : DecidablePred fun x => x s] [inst : Infinite s] :

    Any infinite set of naturals is denumerable.

    Equations
    • One or more equations did not get rendered due to their size.
    def Denumerable.ofEncodableOfInfinite (α : Type u_1) [inst : Encodable α] [inst : Infinite α] :

    An infinite encodable type is denumerable.

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