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
@[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
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
  • One or more equations did not get rendered due to their size.

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
@[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
  • One or more equations did not get rendered due to their size.