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 α ≃ ℕ.

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

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

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

        A denumerable type is equivalent to .

        Equations
          Instances For
            @[instance 100]
            instance Denumerable.instInfinite {α : Type u_1} [Denumerable α] :
            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} [Denumerable α] (e : β α) :

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

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

                    All denumerable types are equivalent.

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

                        If α is denumerable, then so is Option α.

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

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

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

                            A denumerable collection of denumerable types is denumerable.

                            Equations
                              @[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
                              instance Denumerable.prod {α : Type u_1} {β : Type u_2} [Denumerable α] [Denumerable β] :
                              Denumerable (α × β)

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

                              Equations
                                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)

                                The lift of a denumerable type is denumerable.

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

                                  The lift of a denumerable type is denumerable.

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

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

                                    Equations
                                      Instances For

                                        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
                                          Instances For
                                            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
                                            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
                                            theorem Nat.Subtype.lt_succ_self {s : Set } [Infinite s] [DecidablePred fun (x : ) => x s] (x : s) :
                                            x < succ x
                                            theorem Nat.Subtype.lt_succ_iff_le {s : Set } [Infinite s] [DecidablePred fun (x : ) => x s] {x y : s} :
                                            x < 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
                                              Instances For
                                                @[irreducible]
                                                @[simp]
                                                theorem Nat.Subtype.ofNat_range {s : Set } [Infinite s] [DecidablePred fun (x : ) => x s] :
                                                def Nat.Subtype.denumerable (s : Set ) [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
                                                        instance nonempty_equiv_of_countable {α : Type u_1} {β : Type u_2} [Countable α] [Infinite α] [Countable β] [Infinite β] :
                                                        Nonempty (α β)