HepLean 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

Instances For

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

Equations

Cardinal.instCanLiftENatOfENatLeAleph0 = ⋯

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}) => ⊤

Instances For

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.

Instances For

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

Instances For

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.

Instances For