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_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
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.

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
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.