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

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

• ↑(some n) = ↑n
• ↑none = Cardinal.aleph0

instance Cardinal.instCoeENat : Coe ℕ∞ Cardinal.{u_1}

Equations

• Cardinal.instCoeENat = { coe := Cardinal.ofENat }

@[simp]

theorem Cardinal.ofENat_top : ↑⊤ = Cardinal.aleph0

@[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] : ↑(OfNat.ofNat n) = OfNat.ofNat n

theorem Cardinal.ofENat_strictMono : StrictMono Cardinal.ofENat

@[simp]

theorem Cardinal.ofENat_lt_ofENat {m n : ℕ∞} : ↑m < ↑n ↔ m < n

theorem Cardinal.ofENat_lt_ofENat_of_lt {m n : ℕ∞} : m < n → ↑m < ↑n

Alias of the reverse direction of Cardinal.ofENat_lt_ofENat.

@[simp]

theorem Cardinal.ofENat_lt_aleph0 {m : ℕ∞} : ↑m < Cardinal.aleph0 ↔ m < ⊤

@[simp]

theorem Cardinal.ofENat_lt_nat {m : ℕ∞} {n : ℕ} : ↑m < ↑n ↔ m < ↑n

@[simp]

theorem Cardinal.ofENat_lt_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] : ↑m < OfNat.ofNat n ↔ m < OfNat.ofNat n

@[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 : ℕ∞} : OfNat.ofNat m < ↑n ↔ OfNat.ofNat m < n

theorem Cardinal.ofENat_mono : Monotone Cardinal.ofENat

@[simp]

theorem Cardinal.ofENat_le_ofENat {m n : ℕ∞} : ↑m ≤ ↑n ↔ m ≤ n

theorem Cardinal.ofENat_le_ofENat_of_le {m n : ℕ∞} : m ≤ n → ↑m ≤ ↑n

Alias of the reverse direction of Cardinal.ofENat_le_ofENat.

@[simp]

theorem Cardinal.ofENat_le_aleph0 (n : ℕ∞) : ↑n ≤ Cardinal.aleph0

@[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] : ↑m ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n

@[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 : ℕ∞} : OfNat.ofNat m ≤ ↑n ↔ OfNat.ofNat m ≤ n

theorem Cardinal.ofENat_injective : Function.Injective Cardinal.ofENat

@[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] : ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n

@[simp]

theorem Cardinal.ofNat_eq_ofENat {m : ℕ} {n : ℕ∞} [m.AtLeastTwo] : OfNat.ofNat m = ↑n ↔ OfNat.ofNat m = n

@[simp]

theorem Cardinal.lift_ofENat (m : ℕ∞) : Cardinal.lift.{u, v} ↑m = ↑m

@[simp]

theorem Cardinal.lift_lt_ofENat {x : Cardinal.{v}} {m : ℕ∞} : Cardinal.lift.{u, v} x < ↑m ↔ x < ↑m

@[simp]

theorem Cardinal.lift_le_ofENat {x : Cardinal.{v}} {m : ℕ∞} : Cardinal.lift.{u, v} x ≤ ↑m ↔ x ≤ ↑m

@[simp]

theorem Cardinal.lift_eq_ofENat {x : Cardinal.{v}} {m : ℕ∞} : Cardinal.lift.{u, v} x = ↑m ↔ x = ↑m

@[simp]

theorem Cardinal.ofENat_lt_lift {x : Cardinal.{v}} {m : ℕ∞} : ↑m < Cardinal.lift.{u, v} x ↔ ↑m < x

@[simp]

theorem Cardinal.ofENat_le_lift {x : Cardinal.{v}} {m : ℕ∞} : ↑m ≤ Cardinal.lift.{u, v} x ↔ ↑m ≤ x

@[simp]

theorem Cardinal.ofENat_eq_lift {x : Cardinal.{v}} {m : ℕ∞} : ↑m = Cardinal.lift.{u, v} x ↔ ↑m = x

@[simp]

theorem Cardinal.range_ofENat : Set.range Cardinal.ofENat = Set.Iic Cardinal.aleph0

instance Cardinal.instCanLiftENatOfENatLeAleph0 : CanLift Cardinal.{u_1} ℕ∞ Cardinal.ofENat fun (x : Cardinal.{u_1}) => x ≤ Cardinal.aleph0

noncomputable def Cardinal.toENatAux : Cardinal.{u} → ℕ∞

Unbundled version of Cardinal.toENat.

Equations

• Cardinal.toENatAux = Function.extend Nat.cast Nat.cast fun (x : Cardinal.{?u.8}) => ⊤

theorem Cardinal.toENatAux_nat (n : ℕ) : (↑n).toENatAux = ↑n

theorem Cardinal.toENatAux_zero : Cardinal.toENatAux 0 = 0

theorem Cardinal.toENatAux_eq_top {a : Cardinal.{u_1}} (ha : Cardinal.aleph0 ≤ a) : a.toENatAux = ⊤

theorem Cardinal.toENatAux_ofENat (n : ℕ∞) : (↑n).toENatAux = n

theorem Cardinal.toENatAux_gc : GaloisConnection Cardinal.ofENat Cardinal.toENatAux

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

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.

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.

@[simp]

theorem Cardinal.toENat_ofENat (n : ℕ∞) : Cardinal.toENat ↑n = n

@[simp]

theorem Cardinal.toENat_comp_ofENat : ⇑Cardinal.toENat ∘ Cardinal.ofENat = id

noncomputable def Cardinal.gciENat : GaloisCoinsertion Cardinal.ofENat ⇑Cardinal.toENat

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

Equations

• Cardinal.gciENat = Cardinal.enat_gc.toGaloisCoinsertion Cardinal.gciENat.proof_1

theorem Cardinal.toENat_strictMonoOn : StrictMonoOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)

theorem Cardinal.toENat_injOn : Set.InjOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)

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

theorem Cardinal.toENat_congr {α : Type u} {β : Type v} (e : α ≃ β) : Cardinal.toENat (Cardinal.mk α) = Cardinal.toENat (Cardinal.mk β)

theorem Cardinal.toENat_le_iff_of_le_aleph0 {c c' : Cardinal.{u_1}} (h : c ≤ Cardinal.aleph0) : Cardinal.toENat c ≤ Cardinal.toENat c' ↔ c ≤ c'

theorem Cardinal.toENat_le_iff_of_lt_aleph0 {c c' : Cardinal.{u_1}} (hc' : c' < Cardinal.aleph0) : Cardinal.toENat c ≤ Cardinal.toENat c' ↔ c ≤ c'

theorem Cardinal.toENat_eq_iff_of_le_aleph0 {c c' : Cardinal.{u_1}} (hc : c ≤ Cardinal.aleph0) (hc' : c' ≤ Cardinal.aleph0) : Cardinal.toENat c = Cardinal.toENat c' ↔ c = c'

@[simp]

theorem Cardinal.ofENat_add (m n : ℕ∞) : ↑(m + n) = ↑m + ↑n

@[simp]

theorem Cardinal.aleph0_add_ofENat (m : ℕ∞) : Cardinal.aleph0 + ↑m = Cardinal.aleph0

@[simp]

theorem Cardinal.ofENat_add_aleph0 (m : ℕ∞) : ↑m + Cardinal.aleph0 = Cardinal.aleph0

@[simp]

theorem Cardinal.ofENat_mul_aleph0 {m : ℕ∞} (hm : m ≠ 0) : ↑m * Cardinal.aleph0 = Cardinal.aleph0

@[simp]

theorem Cardinal.aleph0_mul_ofENat {m : ℕ∞} (hm : m ≠ 0) : Cardinal.aleph0 * ↑m = Cardinal.aleph0

@[simp]

theorem Cardinal.ofENat_mul (m n : ℕ∞) : ↑(m * n) = ↑m * ↑n

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.