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

source
def Cardinal.ofENat :
ℕ∞ → Cardinal.{u_1}

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

See also Cardinal.ofENatHom for a bundled homomorphism version.

Equations
  • ↑x = match x with | some n => ↑n | none => Cardinal.aleph0
Instances For
    source
    instance Cardinal.instCoeENatCardinal :
    Coe ℕ∞ Cardinal.{u_1}
    Equations
    source
    @[simp]
    theorem Cardinal.ofENat_top :
    ↑⊤ = Cardinal.aleph0
    source
    @[simp]
    theorem Cardinal.ofENat_nat (n : ℕ) :
    ↑↑n = ↑n
    source
    @[simp]
    theorem Cardinal.ofENat_zero :
    ↑0 = 0
    source
    @[simp]
    theorem Cardinal.ofENat_one :
    ↑1 = 1
    source
    @[simp]
    theorem Cardinal.ofENat_ofNat (n : ℕ) [Nat.AtLeastTwo n] :
    ↑(OfNat.ofNat n) = OfNat.ofNat n
    source
    theorem Cardinal.ofENat_strictMono :
    StrictMono Cardinal.ofENat
    source
    @[simp]
    theorem Cardinal.ofENat_lt_ofENat {m : ℕ∞} {n : ℕ∞} :
    ↑m < ↑n ↔ m < n
    source
    theorem Cardinal.ofENat_lt_ofENat_of_lt {m : ℕ∞} {n : ℕ∞} :
    m < n → ↑m < ↑n

    Alias of the reverse direction of Cardinal.ofENat_lt_ofENat.

    source
    @[simp]
    theorem Cardinal.ofENat_lt_aleph0 {m : ℕ∞} :
    ↑m < Cardinal.aleph0 ↔ m < ⊤
    source
    @[simp]
    theorem Cardinal.ofENat_lt_nat {m : ℕ∞} {n : ℕ} :
    ↑m < ↑n ↔ m < ↑n
    source
    @[simp]
    theorem Cardinal.ofENat_lt_ofNat {m : ℕ∞} {n : ℕ} [Nat.AtLeastTwo n] :
    ↑m < OfNat.ofNat n ↔ m < OfNat.ofNat n
    source
    @[simp]
    theorem Cardinal.nat_lt_ofENat {m : ℕ} {n : ℕ∞} :
    ↑m < ↑n ↔ ↑m < n
    source
    @[simp]
    theorem Cardinal.ofENat_pos {m : ℕ∞} :
    0 < ↑m ↔ 0 < m
    source
    @[simp]
    theorem Cardinal.one_lt_ofENat {m : ℕ∞} :
    1 < ↑m ↔ 1 < m
    source
    @[simp]
    theorem Cardinal.ofNat_lt_ofENat {m : ℕ} [Nat.AtLeastTwo m] {n : ℕ∞} :
    OfNat.ofNat m < ↑n ↔ OfNat.ofNat m < n
    source
    theorem Cardinal.ofENat_mono :
    Monotone Cardinal.ofENat
    source
    @[simp]
    theorem Cardinal.ofENat_le_ofENat {m : ℕ∞} {n : ℕ∞} :
    ↑m ≤ ↑n ↔ m ≤ n
    source
    theorem Cardinal.ofENat_le_ofENat_of_le {m : ℕ∞} {n : ℕ∞} :
    m ≤ n → ↑m ≤ ↑n

    Alias of the reverse direction of Cardinal.ofENat_le_ofENat.

    source
    @[simp]
    theorem Cardinal.ofENat_le_aleph0 (n : ℕ∞) :
    ↑n ≤ Cardinal.aleph0
    source
    @[simp]
    theorem Cardinal.ofENat_le_nat {m : ℕ∞} {n : ℕ} :
    ↑m ≤ ↑n ↔ m ≤ ↑n
    source
    @[simp]
    theorem Cardinal.ofENat_le_one {m : ℕ∞} :
    ↑m ≤ 1 ↔ m ≤ 1
    source
    @[simp]
    theorem Cardinal.ofENat_le_ofNat {m : ℕ∞} {n : ℕ} [Nat.AtLeastTwo n] :
    ↑m ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n
    source
    @[simp]
    theorem Cardinal.nat_le_ofENat {m : ℕ} {n : ℕ∞} :
    ↑m ≤ ↑n ↔ ↑m ≤ n
    source
    @[simp]
    theorem Cardinal.one_le_ofENat {n : ℕ∞} :
    1 ≤ ↑n ↔ 1 ≤ n
    source
    @[simp]
    theorem Cardinal.ofNat_le_ofENat {m : ℕ} [Nat.AtLeastTwo m] {n : ℕ∞} :
    OfNat.ofNat m ≤ ↑n ↔ OfNat.ofNat m ≤ n
    source
    theorem Cardinal.ofENat_injective :
    Function.Injective Cardinal.ofENat
    source
    @[simp]
    theorem Cardinal.ofENat_inj {m : ℕ∞} {n : ℕ∞} :
    ↑m = ↑n ↔ m = n
    source
    @[simp]
    theorem Cardinal.ofENat_eq_nat {m : ℕ∞} {n : ℕ} :
    ↑m = ↑n ↔ m = ↑n
    source
    @[simp]
    theorem Cardinal.nat_eq_ofENat {m : ℕ} {n : ℕ∞} :
    ↑m = ↑n ↔ ↑m = n
    source
    @[simp]
    theorem Cardinal.ofENat_eq_zero {m : ℕ∞} :
    ↑m = 0 ↔ m = 0
    source
    @[simp]
    theorem Cardinal.zero_eq_ofENat {m : ℕ∞} :
    0 = ↑m ↔ m = 0
    source
    @[simp]
    theorem Cardinal.ofENat_eq_one {m : ℕ∞} :
    ↑m = 1 ↔ m = 1
    source
    @[simp]
    theorem Cardinal.one_eq_ofENat {m : ℕ∞} :
    1 = ↑m ↔ m = 1
    source
    @[simp]
    theorem Cardinal.ofENat_eq_ofNat {m : ℕ∞} {n : ℕ} [Nat.AtLeastTwo n] :
    ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
    source
    @[simp]
    theorem Cardinal.ofNat_eq_ofENat {m : ℕ} {n : ℕ∞} [Nat.AtLeastTwo m] :
    OfNat.ofNat m = ↑n ↔ OfNat.ofNat m = n
    source
    @[simp]
    theorem Cardinal.lift_ofENat (m : ℕ∞) :
    Cardinal.lift.{u, v} ↑m = ↑m
    source
    @[simp]
    theorem Cardinal.lift_lt_ofENat {x : Cardinal.{v}} {m : ℕ∞} :
    Cardinal.lift.{u, v} x < ↑m ↔ x < ↑m
    source
    @[simp]
    theorem Cardinal.lift_le_ofENat {x : Cardinal.{v}} {m : ℕ∞} :
    Cardinal.lift.{u, v} x ≤ ↑m ↔ x ≤ ↑m
    source
    @[simp]
    theorem Cardinal.lift_eq_ofENat {x : Cardinal.{v}} {m : ℕ∞} :
    Cardinal.lift.{u, v} x = ↑m ↔ x = ↑m
    source
    @[simp]
    theorem Cardinal.ofENat_lt_lift {x : Cardinal.{v}} {m : ℕ∞} :
    ↑m < Cardinal.lift.{u, v} x ↔ ↑m < x
    source
    @[simp]
    theorem Cardinal.ofENat_le_lift {x : Cardinal.{v}} {m : ℕ∞} :
    ↑m ≤ Cardinal.lift.{u, v} x ↔ ↑m ≤ x
    source
    @[simp]
    theorem Cardinal.ofENat_eq_lift {x : Cardinal.{v}} {m : ℕ∞} :
    ↑m = Cardinal.lift.{u, v} x ↔ ↑m = x
    source
    @[simp]
    theorem Cardinal.range_ofENat :
    Set.range Cardinal.ofENat = Set.Iic Cardinal.aleph0
    source
    instance Cardinal.instCanLiftCardinalENatOfENatLeInstLECardinalAleph0 :
    CanLift Cardinal.{u_1} ℕ∞ Cardinal.ofENat fun (x : Cardinal.{u_1}) => x ≤ Cardinal.aleph0
    Equations
    source
    noncomputable def Cardinal.toENatAux :
    Cardinal.{u} → ℕ∞

    Unbundled version of Cardinal.toENat.

    Equations
    Instances For
      source
      theorem Cardinal.toENatAux_nat (n : ℕ) :
      Cardinal.toENatAux ↑n = ↑n
      source
      theorem Cardinal.toENatAux_zero :
      Cardinal.toENatAux 0 = 0
      source
      theorem Cardinal.toENatAux_eq_top {a : Cardinal.{u_1}} (ha : Cardinal.aleph0 ≤ a) :
      Cardinal.toENatAux a = ⊤
      source
      theorem Cardinal.toENatAux_ofENat (n : ℕ∞) :
      Cardinal.toENatAux ↑n = n
      source
      theorem Cardinal.toENatAux_gc :
      GaloisConnection Cardinal.ofENat Cardinal.toENatAux
      source
      theorem Cardinal.toENatAux_le_nat {x : Cardinal.{u_1}} {n : ℕ} :
      Cardinal.toENatAux x ≤ ↑n ↔ x ≤ ↑n
      source
      theorem Cardinal.toENatAux_eq_nat {x : Cardinal.{u_1}} {n : ℕ} :
      Cardinal.toENatAux x = ↑n ↔ x = ↑n
      source
      theorem Cardinal.toENatAux_eq_zero {x : Cardinal.{u_1}} :
      Cardinal.toENatAux x = 0 ↔ x = 0
      source
      noncomputable def Cardinal.toENat :
      Cardinal.{u} →+*o ℕ∞

      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
        source
        theorem Cardinal.enat_gc :
        GaloisConnection Cardinal.ofENat ⇑Cardinal.toENat

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

        source
        @[simp]
        theorem Cardinal.toENat_ofENat (n : ℕ∞) :
        Cardinal.toENat ↑n = n
        source
        @[simp]
        theorem Cardinal.toENat_comp_ofENat :
        ⇑Cardinal.toENat ∘ Cardinal.ofENat = id
        source
        noncomputable def Cardinal.gciENat :
        GaloisCoinsertion Cardinal.ofENat ⇑Cardinal.toENat

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

        Equations
        Instances For
          source
          theorem Cardinal.toENat_strictMonoOn :
          StrictMonoOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)
          source
          theorem Cardinal.toENat_injOn :
          Set.InjOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)
          source
          theorem Cardinal.ofENat_toENat_le (a : Cardinal.{u_1}) :
          ↑(Cardinal.toENat a) ≤ a
          source
          @[simp]
          theorem Cardinal.ofENat_toENat_eq_self {a : Cardinal.{u_1}} :
          ↑(Cardinal.toENat a) = a ↔ a ≤ Cardinal.aleph0
          source
          @[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.

          source
          theorem Cardinal.toENat_nat (n : ℕ) :
          Cardinal.toENat ↑n = ↑n
          source
          @[simp]
          theorem Cardinal.toENat_le_nat {a : Cardinal.{u_1}} {n : ℕ} :
          Cardinal.toENat a ≤ ↑n ↔ a ≤ ↑n
          source
          @[simp]
          theorem Cardinal.toENat_eq_nat {a : Cardinal.{u_1}} {n : ℕ} :
          Cardinal.toENat a = ↑n ↔ a = ↑n
          source
          @[simp]
          theorem Cardinal.toENat_eq_zero {a : Cardinal.{u_1}} :
          Cardinal.toENat a = 0 ↔ a = 0
          source
          @[simp]
          theorem Cardinal.toENat_le_one {a : Cardinal.{u_1}} :
          Cardinal.toENat a ≤ 1 ↔ a ≤ 1
          source
          @[simp]
          theorem Cardinal.toENat_eq_one {a : Cardinal.{u_1}} :
          Cardinal.toENat a = 1 ↔ a = 1
          source
          @[simp]
          theorem Cardinal.toENat_le_ofNat {a : Cardinal.{u_1}} {n : ℕ} [Nat.AtLeastTwo n] :
          Cardinal.toENat a ≤ OfNat.ofNat n ↔ a ≤ OfNat.ofNat n
          source
          @[simp]
          theorem Cardinal.toENat_eq_ofNat {a : Cardinal.{u_1}} {n : ℕ} [Nat.AtLeastTwo n] :
          Cardinal.toENat a = OfNat.ofNat n ↔ a = OfNat.ofNat n
          source
          @[simp]
          theorem Cardinal.toENat_eq_top {a : Cardinal.{u_1}} :
          Cardinal.toENat a = ⊤ ↔ Cardinal.aleph0 ≤ a
          source
          @[simp]
          theorem Cardinal.toENat_lift {a : Cardinal.{v}} :
          Cardinal.toENat (Cardinal.lift.{u, v} a) = Cardinal.toENat a
          source
          @[simp]
          theorem Cardinal.ofENat_add (m : ℕ∞) (n : ℕ∞) :
          ↑(m + n) = ↑m + ↑n
          source
          @[simp]
          theorem Cardinal.aleph0_add_ofENat (m : ℕ∞) :
          Cardinal.aleph0 + ↑m = Cardinal.aleph0
          source
          @[simp]
          theorem Cardinal.ofENat_add_aleph0 (m : ℕ∞) :
          ↑m + Cardinal.aleph0 = Cardinal.aleph0
          source
          @[simp]
          theorem Cardinal.ofENat_mul_aleph0 {m : ℕ∞} (hm : m ≠ 0) :
          ↑m * Cardinal.aleph0 = Cardinal.aleph0
          source
          @[simp]
          theorem Cardinal.aleph0_mul_ofENat {m : ℕ∞} (hm : m ≠ 0) :
          Cardinal.aleph0 * ↑m = Cardinal.aleph0
          source
          @[simp]
          theorem Cardinal.ofENat_mul (m : ℕ∞) (n : ℕ∞) :
          ↑(m * n) = ↑m * ↑n
          source
          def Cardinal.ofENatHom :
          ℕ∞ →+*o Cardinal.{u_1}

          The coercion Cardinal.ofENat as a bundled homomorphism.

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