Documentation

Mathlib.SetTheory.Cardinal.ENat

Conversion between Cardinal and ℕ∞ #

In this file we define a coercion Cardinal.ofENat : ℕ∞ → Cardinal and a projection Cardinal.toENat : Cardinal →+*o ℕ∞. We also prove basic theorems about these definitions.

Implementation notes #

We define Cardinal.ofENat as a function instead of a bundled homomorphism so that we can use it as a coercion and delaborate its application to ↑n.

We define Cardinal.toENat as a bundled homomorphism so that we can use all the theorems about homomorphisms without specializing them to this function. Since it is not registered as a coercion, the argument about delaboration does not apply.

Keywords #

set theory, cardinals, extended natural numbers

Coercion ℕ∞ → Cardinal. It sends natural numbers to natural numbers and to ℵ₀.

See also Cardinal.ofENatHom for a bundled homomorphism version.

Equations
    Instances For
      @[simp]
      theorem Cardinal.ofENat_nat (n : ) :
      n = n
      @[simp]
      theorem Cardinal.ofENat_zero :
      0 = 0
      @[simp]
      theorem Cardinal.ofENat_one :
      1 = 1
      @[simp]
      theorem Cardinal.ofENat_lt_ofENat {m n : ℕ∞} :
      m < n m < n
      theorem Cardinal.ofENat_lt_ofENat_of_lt {m n : ℕ∞} :
      m < nm < n

      Alias of the reverse direction of Cardinal.ofENat_lt_ofENat.

      @[simp]
      @[simp]
      theorem Cardinal.ofENat_lt_nat {m : ℕ∞} {n : } :
      m < n m < n
      @[simp]
      @[simp]
      theorem Cardinal.nat_lt_ofENat {m : } {n : ℕ∞} :
      m < n m < n
      @[simp]
      theorem Cardinal.ofENat_pos {m : ℕ∞} :
      0 < m 0 < m
      @[simp]
      theorem Cardinal.one_lt_ofENat {m : ℕ∞} :
      1 < m 1 < m
      @[simp]
      @[simp]
      theorem Cardinal.ofENat_le_ofENat {m n : ℕ∞} :
      m n m n
      theorem Cardinal.ofENat_le_ofENat_of_le {m n : ℕ∞} :
      m nm n

      Alias of the reverse direction of Cardinal.ofENat_le_ofENat.

      @[simp]
      @[simp]
      theorem Cardinal.ofENat_le_nat {m : ℕ∞} {n : } :
      m n m n
      @[simp]
      theorem Cardinal.ofENat_le_one {m : ℕ∞} :
      m 1 m 1
      @[simp]
      theorem Cardinal.nat_le_ofENat {m : } {n : ℕ∞} :
      m n m n
      @[simp]
      theorem Cardinal.one_le_ofENat {n : ℕ∞} :
      1 n 1 n
      @[simp]
      theorem Cardinal.ofENat_inj {m n : ℕ∞} :
      m = n m = n
      @[simp]
      theorem Cardinal.ofENat_eq_nat {m : ℕ∞} {n : } :
      m = n m = n
      @[simp]
      theorem Cardinal.nat_eq_ofENat {m : } {n : ℕ∞} :
      m = n m = n
      @[simp]
      theorem Cardinal.ofENat_eq_zero {m : ℕ∞} :
      m = 0 m = 0
      @[simp]
      theorem Cardinal.zero_eq_ofENat {m : ℕ∞} :
      0 = m m = 0
      @[simp]
      theorem Cardinal.ofENat_eq_one {m : ℕ∞} :
      m = 1 m = 1
      @[simp]
      theorem Cardinal.one_eq_ofENat {m : ℕ∞} :
      1 = m m = 1
      @[simp]
      @[simp]
      @[simp]
      theorem Cardinal.lift_ofENat (m : ℕ∞) :
      lift.{u, v} m = m
      @[simp]
      theorem Cardinal.lift_lt_ofENat {x : Cardinal.{v}} {m : ℕ∞} :
      lift.{u, v} x < m x < m
      @[simp]
      theorem Cardinal.lift_le_ofENat {x : Cardinal.{v}} {m : ℕ∞} :
      lift.{u, v} x m x m
      @[simp]
      theorem Cardinal.lift_eq_ofENat {x : Cardinal.{v}} {m : ℕ∞} :
      lift.{u, v} x = m x = m
      @[simp]
      theorem Cardinal.ofENat_lt_lift {x : Cardinal.{v}} {m : ℕ∞} :
      m < lift.{u, v} x m < x
      @[simp]
      theorem Cardinal.ofENat_le_lift {x : Cardinal.{v}} {m : ℕ∞} :
      m lift.{u, v} x m x
      @[simp]
      theorem Cardinal.ofENat_eq_lift {x : Cardinal.{v}} {m : ℕ∞} :
      m = lift.{u, v} x m = x
      noncomputable def Cardinal.toENatAux :

      Unbundled version of Cardinal.toENat.

      Equations
        Instances For
          theorem Cardinal.toENatAux_nat (n : ) :
          (↑n).toENatAux = n

          Projection from cardinals to ℕ∞. Sends all infinite cardinals to .

          We define this function as a bundled monotone ring homomorphism.

          Equations
            Instances For

              The coercion Cardinal.ofENat and the projection Cardinal.toENat form a Galois connection. See also Cardinal.gciENat.

              @[simp]
              theorem Cardinal.toENat_ofENat (n : ℕ∞) :
              toENat n = n

              The coercion Cardinal.ofENat and the projection Cardinal.toENat form a Galois coinsertion.

              Equations
                Instances For
                  @[simp]
                  theorem Cardinal.ofENat_toENat {a : Cardinal.{u_1}} :
                  a aleph0(toENat a) = a

                  Alias of the reverse direction of Cardinal.ofENat_toENat_eq_self.

                  theorem Cardinal.toENat_nat (n : ) :
                  toENat n = n
                  @[simp]
                  theorem Cardinal.toENat_le_nat {a : Cardinal.{u_1}} {n : } :
                  toENat a n a n
                  @[simp]
                  theorem Cardinal.toENat_eq_nat {a : Cardinal.{u_1}} {n : } :
                  toENat a = n a = n
                  @[simp]
                  @[simp]
                  theorem Cardinal.toENat_congr {α : Type u} {β : Type v} (e : α β) :
                  toENat (mk α) = toENat (mk β)
                  @[simp]
                  theorem Cardinal.ofENat_add (m n : ℕ∞) :
                  ↑(m + n) = m + n
                  @[simp]
                  theorem Cardinal.ofENat_mul_aleph0 {m : ℕ∞} (hm : m 0) :
                  @[simp]
                  theorem Cardinal.aleph0_mul_ofENat {m : ℕ∞} (hm : m 0) :
                  @[simp]
                  theorem Cardinal.ofENat_mul (m n : ℕ∞) :
                  ↑(m * n) = m * n

                  The coercion Cardinal.ofENat as a bundled homomorphism.

                  Equations
                    Instances For