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

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 :

↑⊤ = 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 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 < 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 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 ≤ 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 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 : ℕ∞) :

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

@[simp]

theorem Cardinal.range_ofENat :

Set.range ofENat = Set.Iic aleph0

instance Cardinal.instCanLiftENatOfENatLeAleph0 :

CanLift Cardinal.{u_1} ℕ∞ ofENat fun (x : Cardinal.{u_1}) => x ≤ 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 :

toENatAux 0 = 0

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

a.toENatAux = ⊤

theorem Cardinal.toENatAux_ofENat (n : ℕ∞) :

(↑n).toENatAux = n

theorem Cardinal.toENatAux_gc :

GaloisConnection ofENat 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 ofENat ⇑toENat

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

⇑toENat ∘ ofENat = id

noncomputable def Cardinal.gciENat :

GaloisCoinsertion ofENat ⇑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 (⇑toENat) (Set.Iic aleph0)

theorem Cardinal.toENat_injOn :

Set.InjOn (⇑toENat) (Set.Iic aleph0)

theorem Cardinal.ofENat_toENat_le (a : Cardinal.{u_1}) :

↑(toENat a) ≤ a

@[simp]

theorem Cardinal.ofENat_toENat_eq_self {a : Cardinal.{u_1}} :

↑(toENat a) = a ↔ a ≤ aleph0

@[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]

theorem Cardinal.toENat_eq_zero {a : Cardinal.{u_1}} :

toENat a = 0 ↔ a = 0

@[simp]

theorem Cardinal.toENat_le_one {a : Cardinal.{u_1}} :

toENat a ≤ 1 ↔ a ≤ 1

@[simp]

theorem Cardinal.toENat_eq_one {a : Cardinal.{u_1}} :

toENat a = 1 ↔ a = 1

@[simp]

theorem Cardinal.toENat_le_ofNat {a : Cardinal.{u_1}} {n : ℕ} [n.AtLeastTwo] :

toENat a ≤ OfNat.ofNat n ↔ a ≤ OfNat.ofNat n

@[simp]

theorem Cardinal.toENat_eq_ofNat {a : Cardinal.{u_1}} {n : ℕ} [n.AtLeastTwo] :

toENat a = OfNat.ofNat n ↔ a = OfNat.ofNat n

@[simp]

theorem Cardinal.toENat_eq_top {a : Cardinal.{u_1}} :

toENat a = ⊤ ↔ aleph0 ≤ a

theorem Cardinal.toENat_ne_top {a : Cardinal.{u_1}} :

toENat a ≠ ⊤ ↔ a < aleph0

@[simp]

theorem Cardinal.toENat_lt_top {a : Cardinal.{u_1}} :

toENat a < ⊤ ↔ a < aleph0

@[simp]

theorem Cardinal.toENat_lift {a : Cardinal.{v}} :

toENat (lift.{u, v} a) = toENat a

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

toENat (mk α) = toENat (mk β)

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

toENat c ≤ toENat c' ↔ c ≤ c'

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

toENat c ≤ toENat c' ↔ c ≤ c'

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

toENat c = toENat c' ↔ c = c'

@[simp]

theorem Cardinal.ofENat_add (m n : ℕ∞) :

↑(m + n) = ↑m + ↑n

@[simp]

theorem Cardinal.aleph0_add_ofENat (m : ℕ∞) :

aleph0 + ↑m = aleph0

@[simp]

theorem Cardinal.ofENat_add_aleph0 (m : ℕ∞) :

↑m + aleph0 = aleph0

@[simp]

theorem Cardinal.ofENat_mul_aleph0 {m : ℕ∞} (hm : m ≠ 0) :

↑m * aleph0 = aleph0

@[simp]

theorem Cardinal.aleph0_mul_ofENat {m : ℕ∞} (hm : m ≠ 0) :

aleph0 * ↑m = 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.