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_ofNat (n : ) [n.AtLeastTwo] :
    @[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]
    theorem Cardinal.ofENat_lt_nat {m : ℕ∞} {n : } :
    m < n m < n
    @[simp]
    theorem Cardinal.ofENat_lt_ofNat {m : ℕ∞} {n : } [n.AtLeastTwo] :
    @[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]
    theorem Cardinal.ofNat_lt_ofENat {m : } [m.AtLeastTwo] {n : ℕ∞} :
    @[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]
    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.ofENat_le_ofNat {m : ℕ∞} {n : } [n.AtLeastTwo] :
    @[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.ofNat_le_ofENat {m : } [m.AtLeastTwo] {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]
    theorem Cardinal.ofENat_eq_ofNat {m : ℕ∞} {n : } [n.AtLeastTwo] :
    @[simp]
    theorem Cardinal.ofNat_eq_ofENat {m : } {n : ℕ∞} [m.AtLeastTwo] :
    @[simp]
    @[simp]
    @[simp]
    @[simp]
    @[simp]
    noncomputable def Cardinal.toENatAux :

    Unbundled version of Cardinal.toENat.

    Equations
    Instances For
      theorem Cardinal.toENatAux_nat (n : ) :
      (↑n).toENatAux = n
      theorem Cardinal.toENatAux_ofENat (n : ℕ∞) :
      (↑n).toENatAux = n
      theorem Cardinal.toENatAux_le_nat {x : Cardinal.{u_1}} {n : } :
      x.toENatAux n x n
      theorem Cardinal.toENatAux_eq_nat {x : Cardinal.{u_1}} {n : } :
      x.toENatAux = n x = n
      theorem Cardinal.toENatAux_eq_zero {x : Cardinal.{u_1}} :
      x.toENatAux = 0 x = 0

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

      We define this function as a bundled monotone ring homomorphism.

      Equations
      • One or more equations did not get rendered due to their size.
      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 : ℕ∞) :
        Cardinal.toENat n = n

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

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

          Alias of the reverse direction of Cardinal.ofENat_toENat_eq_self.

          theorem Cardinal.toENat_nat (n : ) :
          Cardinal.toENat n = n
          @[simp]
          theorem Cardinal.toENat_le_nat {a : Cardinal.{u_1}} {n : } :
          Cardinal.toENat a n a n
          @[simp]
          theorem Cardinal.toENat_eq_nat {a : Cardinal.{u_1}} {n : } :
          Cardinal.toENat a = n a = n
          @[simp]
          theorem Cardinal.toENat_eq_zero {a : Cardinal.{u_1}} :
          Cardinal.toENat a = 0 a = 0
          @[simp]
          theorem Cardinal.toENat_le_one {a : Cardinal.{u_1}} :
          Cardinal.toENat a 1 a 1
          @[simp]
          theorem Cardinal.toENat_eq_one {a : Cardinal.{u_1}} :
          Cardinal.toENat a = 1 a = 1
          @[simp]
          theorem Cardinal.toENat_le_ofNat {a : Cardinal.{u_1}} {n : } [n.AtLeastTwo] :
          Cardinal.toENat a OfNat.ofNat n a OfNat.ofNat n
          @[simp]
          theorem Cardinal.toENat_eq_ofNat {a : Cardinal.{u_1}} {n : } [n.AtLeastTwo] :
          Cardinal.toENat a = OfNat.ofNat n a = OfNat.ofNat n
          @[simp]
          theorem Cardinal.toENat_eq_top {a : Cardinal.{u_1}} :
          Cardinal.toENat a = Cardinal.aleph0 a
          @[simp]
          theorem Cardinal.toENat_lift {a : Cardinal.{v}} :
          Cardinal.toENat (Cardinal.lift.{u, v} a) = Cardinal.toENat a
          @[simp]
          theorem Cardinal.ofENat_add (m : ℕ∞) (n : ℕ∞) :
          (m + n) = m + n
          @[simp]
          theorem Cardinal.ofENat_mul (m : ℕ∞) (n : ℕ∞) :
          (m * n) = m * n

          The coercion Cardinal.ofENat as a bundled homomorphism.

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