Omega, aleph, and beth functions #

The function Ordinal.preOmega enumerates the initial ordinals, i.e. the smallest ordinals with any given cardinality. Thus preOmega n = n, preOmega ω = ω, preOmega (ω + 1) = ω₁, etc. Ordinal.omega is the more standard function which skips over finite ordinals.
The function Cardinal.preAleph is an order isomorphism between ordinals and cardinals. Thus preAleph n = n, preAleph ω = ℵ₀, preAleph (ω + 1) = ℵ₁, etc. Cardinal.aleph is the more standard function which skips over finite ordinals.
The function Cardinal.beth enumerates the Beth cardinals. beth 0 = ℵ₀, beth (succ o) = 2 ^ beth o, and for a limit ordinal o, beth o is the supremum of beth a for a < o.

Notation #

The following notations are scoped to the Ordinal namespace.

ω_ o is notation for Ordinal.omega o. ω₁ is notation for ω_ 1.

The following notations are scoped to the Cardinal namespace.

ℵ_ o is notation for aleph o. ℵ₁ is notation for ℵ_ 1.
ℶ_ o is notation for beth o. The value ℶ_ 1 equals the continuum 𝔠, which is defined in Mathlib.SetTheory.Cardinal.Continuum.

Omega ordinals #

source

def Ordinal.IsInitial (o : Ordinal.{u_1}) :

Prop

An ordinal is initial when it is the first ordinal with a given cardinality.

This is written as o.card.ord = o, i.e. o is the smallest ordinal with cardinality o.card.

Equations

o.IsInitial = (o.card.ord = o)

source

theorem Ordinal.IsInitial.ord_card {o : Ordinal.{u_1}} (h : o.IsInitial) :

o.card.ord = o

source

theorem Ordinal.IsInitial.card_le_card {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (ha : a.IsInitial) :

a.card ≤ b.card ↔ a ≤ b

source

theorem Ordinal.IsInitial.card_lt_card {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (hb : b.IsInitial) :

a.card < b.card ↔ a < b

source

theorem Ordinal.isInitial_ord (c : Cardinal.{u_1}) :

c.ord.IsInitial

source

theorem Ordinal.isInitial_natCast (n : ℕ) :

(↑n).IsInitial

source

theorem Ordinal.isInitial_zero :

Ordinal.IsInitial 0

source

theorem Ordinal.isInitial_one :

Ordinal.IsInitial 1

source

theorem Ordinal.isInitial_omega0 :

Ordinal.omega0.IsInitial

source

theorem Ordinal.not_bddAbove_isInitial :

¬BddAbove {x : Ordinal.{u_1} | x.IsInitial}

source

@[simp]

theorem Ordinal.isInitialIso_apply (x : { x : Ordinal.{u_1} // x.IsInitial }) :

Ordinal.isInitialIso x = (↑x).card

source

@[simp]

theorem Ordinal.isInitialIso_symm_apply_coe (x : Cardinal.{u_1}) :

↑((RelIso.symm Ordinal.isInitialIso) x) = x.ord

source

def Ordinal.isInitialIso :

{ x : Ordinal.{u_1} // x.IsInitial } ≃o Cardinal.{u_1}

Initial ordinals are order-isomorphic to the cardinals.

Equations

One or more equations did not get rendered due to their size.

source

def Ordinal.preOmega :

Ordinal.{u} ↪o Ordinal.{u}

The "pre-omega" function gives the initial ordinals listed by their ordinal index. preOmega n = n, preOmega ω = ω, preOmega (ω + 1) = ω₁, etc.

For the more common omega function skipping over finite ordinals, see Ordinal.omega.

Equations

Ordinal.preOmega = { toFun := Ordinal.enumOrd {x : Ordinal.{?u.8} | x.IsInitial}, inj' := Ordinal.preOmega.proof_1, map_rel_iff' := @Ordinal.preOmega.proof_2 }

source

theorem Ordinal.coe_preOmega :

⇑Ordinal.preOmega = Ordinal.enumOrd {x : Ordinal.{u_1} | x.IsInitial}

source

theorem Ordinal.preOmega_strictMono :

StrictMono ⇑Ordinal.preOmega

source

theorem Ordinal.preOmega_lt_preOmega {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Ordinal.preOmega o₁ < Ordinal.preOmega o₂ ↔ o₁ < o₂

source

theorem Ordinal.preOmega_le_preOmega {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Ordinal.preOmega o₁ ≤ Ordinal.preOmega o₂ ↔ o₁ ≤ o₂

source

theorem Ordinal.preOmega_max (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :

Ordinal.preOmega (max o₁ o₂) = max (Ordinal.preOmega o₁) (Ordinal.preOmega o₂)

source

theorem Ordinal.isInitial_preOmega (o : Ordinal.{u_1}) :

(Ordinal.preOmega o).IsInitial

source

theorem Ordinal.le_preOmega_self (o : Ordinal.{u_1}) :

o ≤ Ordinal.preOmega o

source

@[simp]

theorem Ordinal.preOmega_zero :

Ordinal.preOmega 0 = 0

source

@[simp]

theorem Ordinal.preOmega_natCast (n : ℕ) :

Ordinal.preOmega ↑n = ↑n

source

@[simp]

theorem Ordinal.preOmega_ofNat (n : ℕ) [n.AtLeastTwo] :

Ordinal.preOmega (OfNat.ofNat n) = ↑n

source

theorem Ordinal.preOmega_le_of_forall_lt {o : Ordinal.{u_1}} {a : Ordinal.{u_1}} (ha : a.IsInitial) (H : ∀ b < o, Ordinal.preOmega b < a) :

Ordinal.preOmega o ≤ a

source

theorem Ordinal.isNormal_preOmega :

Ordinal.IsNormal ⇑Ordinal.preOmega

source

@[simp]

theorem Ordinal.range_preOmega :

Set.range ⇑Ordinal.preOmega = {x : Ordinal.{u_1} | x.IsInitial}

source

theorem Ordinal.mem_range_preOmega_iff {x : Ordinal.{u_1}} :

x ∈ Set.range ⇑Ordinal.preOmega ↔ x.IsInitial

source

theorem Ordinal.IsInitial.mem_range_preOmega {x : Ordinal.{u_1}} :

x.IsInitial → x ∈ Set.range ⇑Ordinal.preOmega

Alias of the reverse direction of Ordinal.mem_range_preOmega_iff.

source

@[simp]

theorem Ordinal.preOmega_omega0 :

Ordinal.preOmega Ordinal.omega0 = Ordinal.omega0

source

@[simp]

theorem Ordinal.omega0_le_preOmega_iff {x : Ordinal.{u_1}} :

Ordinal.omega0 ≤ Ordinal.preOmega x ↔ Ordinal.omega0 ≤ x

source

@[simp]

theorem Ordinal.omega0_lt_preOmega_iff {x : Ordinal.{u_1}} :

Ordinal.omega0 < Ordinal.preOmega x ↔ Ordinal.omega0 < x

source

def Ordinal.omega :

Ordinal.{u_1} ↪o Ordinal.{u_1}

The omega function gives the infinite initial ordinals listed by their ordinal index. omega 0 = ω, omega 1 = ω₁ is the first uncountable ordinal, and so on.

This is not to be confused with the first infinite ordinal Ordinal.omega0.

For a version including finite ordinals, see Ordinal.preOmega.

Equations

Ordinal.omega = RelEmbedding.trans (OrderEmbedding.addLeft Ordinal.omega0) Ordinal.preOmega

source

def Ordinal.termω_ :

Lean.ParserDescr

The omega function gives the infinite initial ordinals listed by their ordinal index. omega 0 = ω, omega 1 = ω₁ is the first uncountable ordinal, and so on.

This is not to be confused with the first infinite ordinal Ordinal.omega0.

For a version including finite ordinals, see Ordinal.preOmega.

Equations

Ordinal.termω_ = Lean.ParserDescr.node `Ordinal.termω_ 1024 (Lean.ParserDescr.symbol "ω_ ")

source

def Ordinal.termω₁ :

Lean.ParserDescr

ω₁ is the first uncountable ordinal.

Equations

Ordinal.termω₁ = Lean.ParserDescr.node `Ordinal.termω₁ 1024 (Lean.ParserDescr.symbol "ω₁")

source

theorem Ordinal.omega_eq_preOmega (o : Ordinal.{u_1}) :

Ordinal.omega o = Ordinal.preOmega (Ordinal.omega0 + o)

source

theorem Ordinal.omega_strictMono :

StrictMono ⇑Ordinal.omega

source

theorem Ordinal.omega_lt_omega {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Ordinal.omega o₁ < Ordinal.omega o₂ ↔ o₁ < o₂

source

theorem Ordinal.omega_le_omega {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Ordinal.omega o₁ ≤ Ordinal.omega o₂ ↔ o₁ ≤ o₂

source

theorem Ordinal.omega_max (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :

Ordinal.omega (max o₁ o₂) = max (Ordinal.omega o₁) (Ordinal.omega o₂)

source

theorem Ordinal.isInitial_omega (o : Ordinal.{u_1}) :

(Ordinal.omega o).IsInitial

source

theorem Ordinal.le_omega_self (o : Ordinal.{u_1}) :

o ≤ Ordinal.omega o

source

@[simp]

theorem Ordinal.omega_zero :

Ordinal.omega 0 = Ordinal.omega0

source

theorem Ordinal.omega0_le_omega (o : Ordinal.{u_1}) :

Ordinal.omega0 ≤ Ordinal.omega o

source

theorem Ordinal.omega0_lt_omega1 :

Ordinal.omega0 < Ordinal.omega 1

source

@[deprecated Ordinal.omega0_lt_omega1]

theorem Ordinal.omega_lt_omega1 :

Ordinal.omega0 < Ordinal.omega 1

Alias of Ordinal.omega0_lt_omega1.

source

theorem Ordinal.isNormal_omega :

Ordinal.IsNormal ⇑Ordinal.omega

source

@[simp]

theorem Ordinal.range_omega :

Set.range ⇑Ordinal.omega = {x : Ordinal.{u_1} | Ordinal.omega0 ≤ x ∧ x.IsInitial}

source

theorem Ordinal.mem_range_omega_iff {x : Ordinal.{u_1}} :

x ∈ Set.range ⇑Ordinal.omega ↔ Ordinal.omega0 ≤ x ∧ x.IsInitial

Aleph cardinals #

source

def Cardinal.preAleph :

Ordinal.{u} ≃o Cardinal.{u}

The "pre-aleph" function gives the cardinals listed by their ordinal index. preAleph n = n, preAleph ω = ℵ₀, preAleph (ω + 1) = succ ℵ₀, etc.

For the more common aleph function skipping over finite cardinals, see Cardinal.aleph.

Equations

Cardinal.preAleph = (OrderIso.ofRelIsoLT (RelIso.ofSurjective Cardinal.ord.orderEmbedding.ltEmbedding.collapse.toRelEmbedding Cardinal.preAleph.proof_1)).symm

source

@[simp]

theorem Cardinal.type_cardinal :

(Ordinal.type fun (x1 x2 : Cardinal.{u}) => x1 < x2) = Ordinal.univ.{u, u + 1}

source

@[simp]

theorem Cardinal.mk_cardinal :

Cardinal.mk Cardinal.{u} = Cardinal.univ.{u, u + 1}

source

theorem Cardinal.preAleph_lt_preAleph {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Cardinal.preAleph o₁ < Cardinal.preAleph o₂ ↔ o₁ < o₂

source

theorem Cardinal.preAleph_le_preAleph {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Cardinal.preAleph o₁ ≤ Cardinal.preAleph o₂ ↔ o₁ ≤ o₂

source

theorem Cardinal.preAleph_max (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :

Cardinal.preAleph (max o₁ o₂) = max (Cardinal.preAleph o₁) (Cardinal.preAleph o₂)

source

@[simp]

theorem Cardinal.preAleph_zero :

Cardinal.preAleph 0 = 0

source

@[simp]

theorem Cardinal.preAleph_succ (o : Ordinal.{u_1}) :

Cardinal.preAleph (Order.succ o) = Order.succ (Cardinal.preAleph o)

source

@[simp]

theorem Cardinal.preAleph_nat (n : ℕ) :

Cardinal.preAleph ↑n = ↑n

source

theorem Cardinal.preAleph_pos {o : Ordinal.{u_1}} :

0 < Cardinal.preAleph o ↔ 0 < o

source

@[simp]

theorem Cardinal.lift_preAleph (o : Ordinal.{u}) :

Cardinal.lift.{v, u} (Cardinal.preAleph o) = Cardinal.preAleph (Ordinal.lift.{v, u} o)

source

theorem Cardinal.preAleph_le_of_isLimit {o : Ordinal.{u_1}} (l : o.IsLimit) {c : Cardinal.{u_1}} :

Cardinal.preAleph o ≤ c ↔ ∀ o' < o, Cardinal.preAleph o' ≤ c

source

theorem Cardinal.preAleph_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :

Cardinal.preAleph o = ⨆ (a : ↑(Set.Iio o)), Cardinal.preAleph ↑a

source

@[simp]

theorem Cardinal.preAleph_omega0 :

Cardinal.preAleph Ordinal.omega0 = Cardinal.aleph0

source

@[simp]

theorem Cardinal.aleph0_le_preAleph {o : Ordinal.{u_1}} :

Cardinal.aleph0 ≤ Cardinal.preAleph o ↔ Ordinal.omega0 ≤ o

source

def Cardinal.aleph :

Ordinal.{u_1} ↪o Cardinal.{u_1}

The aleph function gives the infinite cardinals listed by their ordinal index. aleph 0 = ℵ₀, aleph 1 = succ ℵ₀ is the first uncountable cardinal, and so on.

For a version including finite cardinals, see Cardinal.aleph'.

Equations

Cardinal.aleph = RelEmbedding.trans (OrderEmbedding.addLeft Ordinal.omega0) Cardinal.preAleph.toOrderEmbedding

source

def Cardinal.termℵ_ :

Lean.ParserDescr

The aleph function gives the infinite cardinals listed by their ordinal index. aleph 0 = ℵ₀, aleph 1 = succ ℵ₀ is the first uncountable cardinal, and so on.

For a version including finite cardinals, see Cardinal.aleph'.

Equations

Cardinal.termℵ_ = Lean.ParserDescr.node `Cardinal.termℵ_ 1024 (Lean.ParserDescr.symbol "ℵ_ ")

source

def Cardinal.termℵ₁ :

Lean.ParserDescr

ℵ₁ is the first uncountable cardinal.

Equations

Cardinal.termℵ₁ = Lean.ParserDescr.node `Cardinal.termℵ₁ 1024 (Lean.ParserDescr.symbol "ℵ₁")

source

theorem Cardinal.aleph_eq_preAleph (o : Ordinal.{u_1}) :

Cardinal.aleph o = Cardinal.preAleph (Ordinal.omega0 + o)

source

theorem Cardinal.aleph_lt_aleph {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Cardinal.aleph o₁ < Cardinal.aleph o₂ ↔ o₁ < o₂

source

@[deprecated Cardinal.aleph_lt_aleph]

theorem Cardinal.aleph_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Cardinal.aleph o₁ < Cardinal.aleph o₂ ↔ o₁ < o₂

Alias of Cardinal.aleph_lt_aleph.

source

theorem Cardinal.aleph_le_aleph {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Cardinal.aleph o₁ ≤ Cardinal.aleph o₂ ↔ o₁ ≤ o₂

source

@[deprecated Cardinal.aleph_le_aleph]

theorem Cardinal.aleph_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Cardinal.aleph o₁ ≤ Cardinal.aleph o₂ ↔ o₁ ≤ o₂

Alias of Cardinal.aleph_le_aleph.

source

theorem Cardinal.aleph_max (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :

Cardinal.aleph (max o₁ o₂) = max (Cardinal.aleph o₁) (Cardinal.aleph o₂)

source

@[deprecated Cardinal.aleph_max]

theorem Cardinal.max_aleph_eq (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :

max (Cardinal.aleph o₁) (Cardinal.aleph o₂) = Cardinal.aleph (max o₁ o₂)

source

@[simp]

theorem Cardinal.aleph_succ (o : Ordinal.{u_1}) :

Cardinal.aleph (Order.succ o) = Order.succ (Cardinal.aleph o)

source

@[simp]

theorem Cardinal.aleph_zero :

Cardinal.aleph 0 = Cardinal.aleph0

source

@[simp]

theorem Cardinal.lift_aleph (o : Ordinal.{u}) :

Cardinal.lift.{v, u} (Cardinal.aleph o) = Cardinal.aleph (Ordinal.lift.{v, u} o)

source

theorem Cardinal.aleph_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :

Cardinal.aleph o = ⨆ (a : ↑(Set.Iio o)), Cardinal.aleph ↑a

source

theorem Cardinal.aleph0_le_aleph (o : Ordinal.{u_1}) :

Cardinal.aleph0 ≤ Cardinal.aleph o

source

theorem Cardinal.aleph_pos (o : Ordinal.{u_1}) :

0 < Cardinal.aleph o

source

@[simp]

theorem Cardinal.aleph_toNat (o : Ordinal.{u_1}) :

Cardinal.toNat (Cardinal.aleph o) = 0

source

@[simp]

theorem Cardinal.aleph_toPartENat (o : Ordinal.{u_1}) :

Cardinal.toPartENat (Cardinal.aleph o) = ⊤

source

instance Cardinal.nonempty_toType_aleph (o : Ordinal.{u_1}) :

Nonempty (Cardinal.aleph o).ord.toType

Equations

⋯ = ⋯

source

theorem Cardinal.ord_aleph_isLimit (o : Ordinal.{u_1}) :

(Cardinal.aleph o).ord.IsLimit

source

instance Cardinal.instNoMaxOrderToTypeOrdCoeOrderEmbeddingOrdinalAleph (o : Ordinal.{u_1}) :

NoMaxOrder (Cardinal.aleph o).ord.toType

Equations

⋯ = ⋯

source

theorem Cardinal.exists_aleph {c : Cardinal.{u_1}} :

Cardinal.aleph0 ≤ c ↔ ∃ (o : Ordinal.{u_1}), c = Cardinal.aleph o

source

theorem Cardinal.preAleph_isNormal :

Ordinal.IsNormal (Cardinal.ord ∘ ⇑Cardinal.preAleph)

source

theorem Cardinal.aleph_isNormal :

Ordinal.IsNormal (Cardinal.ord ∘ ⇑Cardinal.aleph)

source

theorem Cardinal.succ_aleph0 :

Order.succ Cardinal.aleph0 = Cardinal.aleph 1

source

theorem Cardinal.aleph0_lt_aleph_one :

Cardinal.aleph0 < Cardinal.aleph 1

source

theorem Cardinal.countable_iff_lt_aleph_one {α : Type u_1} (s : Set α) :

s.Countable ↔ Cardinal.mk ↑s < Cardinal.aleph 1

source

@[simp]

theorem Cardinal.aleph1_le_lift {c : Cardinal.{u}} :

Cardinal.aleph 1 ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph 1 ≤ c

source

@[simp]

theorem Cardinal.lift_le_aleph1 {c : Cardinal.{u}} :

Cardinal.lift.{v, u} c ≤ Cardinal.aleph 1 ↔ c ≤ Cardinal.aleph 1

source

@[simp]

theorem Cardinal.aleph1_lt_lift {c : Cardinal.{u}} :

Cardinal.aleph 1 < Cardinal.lift.{v, u} c ↔ Cardinal.aleph 1 < c

source

@[simp]

theorem Cardinal.lift_lt_aleph1 {c : Cardinal.{u}} :

Cardinal.lift.{v, u} c < Cardinal.aleph 1 ↔ c < Cardinal.aleph 1

source

@[simp]

theorem Cardinal.aleph1_eq_lift {c : Cardinal.{u}} :

Cardinal.aleph 1 = Cardinal.lift.{v, u} c ↔ Cardinal.aleph 1 = c

source

@[simp]

theorem Cardinal.lift_eq_aleph1 {c : Cardinal.{u}} :

Cardinal.lift.{v, u} c = Cardinal.aleph 1 ↔ c = Cardinal.aleph 1

source

@[deprecated Cardinal.preAleph]

def Cardinal.aleph' :

Ordinal.{u} ≃o Cardinal.{u}

Alias of Cardinal.preAleph.

The "pre-aleph" function gives the cardinals listed by their ordinal index. preAleph n = n, preAleph ω = ℵ₀, preAleph (ω + 1) = succ ℵ₀, etc.

For the more common aleph function skipping over finite cardinals, see Cardinal.aleph.

Equations

Cardinal.aleph' = Cardinal.preAleph

source

@[deprecated Cardinal.preAleph]

def Cardinal.alephIdx.initialSeg :

(fun (x1 x2 : Cardinal.{u_1}) => x1 < x2) ≼i fun (x1 x2 : Ordinal.{u_1}) => x1 < x2

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ω = ω, alephIdx ℵ₁ = ω + 1 and so on.) In this definition, we register additionally that this function is an initial segment, i.e., it is order preserving and its range is an initial segment of the ordinals. For the basic function version, see alephIdx. For an upgraded version stating that the range is everything, see AlephIdx.rel_iso.

Equations

Cardinal.alephIdx.initialSeg = Cardinal.ord.orderEmbedding.ltEmbedding.collapse

source

@[deprecated Cardinal.preAleph]

def Cardinal.alephIdx.relIso :

(fun (x1 x2 : Cardinal.{u}) => x1 < x2) ≃r fun (x1 x2 : Ordinal.{u}) => x1 < x2

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ℵ₀ = ω, alephIdx ℵ₁ = ω + 1 and so on.) In this version, we register additionally that this function is an order isomorphism between cardinals and ordinals. For the basic function version, see alephIdx.

Equations

Cardinal.alephIdx.relIso = Cardinal.aleph'.symm.toRelIsoLT

source

@[deprecated Cardinal.aleph']

def Cardinal.alephIdx :

Cardinal.{u_1} → Ordinal.{u_1}

Equations

Cardinal.alephIdx = ⇑Cardinal.aleph'.symm

source

@[deprecated]

theorem Cardinal.alephIdx.initialSeg_coe :

⇑Cardinal.alephIdx.initialSeg = Cardinal.alephIdx

source

@[deprecated]

theorem Cardinal.alephIdx_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} :

a.alephIdx < b.alephIdx ↔ a < b

source

@[deprecated]

theorem Cardinal.alephIdx_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} :

a.alephIdx ≤ b.alephIdx ↔ a ≤ b

source

@[deprecated]

theorem Cardinal.alephIdx.init {a : Cardinal.{u_1}} {b : Ordinal.{u_1}} :

b < a.alephIdx → ∃ (c : Cardinal.{u_1}), c.alephIdx = b

source

@[deprecated]

theorem Cardinal.alephIdx.relIso_coe :

⇑Cardinal.alephIdx.relIso = Cardinal.alephIdx

source

@[deprecated Cardinal.aleph']

def Cardinal.Aleph'.relIso :

Ordinal.{u_1} ≃o Cardinal.{u_1}

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = succ ℵ₀, etc. In this version, we register additionally that this function is an order isomorphism between ordinals and cardinals. For the basic function version, see aleph'.

Equations

Cardinal.Aleph'.relIso = Cardinal.aleph'

source

@[deprecated]

theorem Cardinal.aleph'.relIso_coe :

⇑Cardinal.Aleph'.relIso = ⇑Cardinal.aleph'

source

@[deprecated Cardinal.preAleph_lt_preAleph]

theorem Cardinal.aleph'_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Cardinal.aleph' o₁ < Cardinal.aleph' o₂ ↔ o₁ < o₂

source

@[deprecated Cardinal.preAleph_le_preAleph]

theorem Cardinal.aleph'_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :

Cardinal.aleph' o₁ ≤ Cardinal.aleph' o₂ ↔ o₁ ≤ o₂

source

@[deprecated Cardinal.preAleph_max]

theorem Cardinal.aleph'_max (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :

Cardinal.aleph' (max o₁ o₂) = max (Cardinal.aleph' o₁) (Cardinal.aleph' o₂)

source

@[deprecated]

theorem Cardinal.aleph'_alephIdx (c : Cardinal.{u_1}) :

Cardinal.aleph' c.alephIdx = c

source

@[deprecated]

theorem Cardinal.alephIdx_aleph' (o : Ordinal.{u_1}) :

(Cardinal.aleph' o).alephIdx = o

source

@[deprecated Cardinal.preAleph_zero]

theorem Cardinal.aleph'_zero :

Cardinal.aleph' 0 = 0

source

@[deprecated Cardinal.preAleph_succ]

theorem Cardinal.aleph'_succ (o : Ordinal.{u_1}) :

Cardinal.aleph' (Order.succ o) = Order.succ (Cardinal.aleph' o)

source

@[deprecated Cardinal.preAleph_nat]

theorem Cardinal.aleph'_nat (n : ℕ) :

Cardinal.aleph' ↑n = ↑n

source

@[deprecated Cardinal.lift_preAleph]

theorem Cardinal.lift_aleph' (o : Ordinal.{u}) :

Cardinal.lift.{v, u} (Cardinal.aleph' o) = Cardinal.aleph' (Ordinal.lift.{v, u} o)

source

@[deprecated Cardinal.preAleph_le_of_isLimit]

theorem Cardinal.aleph'_le_of_limit {o : Ordinal.{u_1}} (l : o.IsLimit) {c : Cardinal.{u_1}} :

Cardinal.aleph' o ≤ c ↔ ∀ o' < o, Cardinal.aleph' o' ≤ c

source

@[deprecated Cardinal.preAleph_limit]

theorem Cardinal.aleph'_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :

Cardinal.aleph' o = ⨆ (a : ↑(Set.Iio o)), Cardinal.aleph' ↑a

source

@[deprecated Cardinal.preAleph_omega0]

theorem Cardinal.aleph'_omega0 :

Cardinal.aleph' Ordinal.omega0 = Cardinal.aleph0

source

@[deprecated Cardinal.aleph'_omega0]

theorem Cardinal.aleph'_omega :

Cardinal.aleph' Ordinal.omega0 = Cardinal.aleph0

Alias of Cardinal.aleph'_omega0.

source

@[deprecated Cardinal.aleph']

def Cardinal.aleph'Equiv :

Ordinal.{u_1} ≃ Cardinal.{u_1}

aleph' and aleph_idx form an equivalence between Ordinal and Cardinal

Equations

Cardinal.aleph'Equiv = { toFun := ⇑Cardinal.aleph', invFun := Cardinal.alephIdx, left_inv := Cardinal.alephIdx_aleph', right_inv := Cardinal.aleph'_alephIdx }

source

theorem Cardinal.aleph_eq_aleph' (o : Ordinal.{u_1}) :

Cardinal.aleph o = Cardinal.preAleph (Ordinal.omega0 + o)

source

@[deprecated Cardinal.aleph0_le_preAleph]

theorem Cardinal.aleph0_le_aleph' {o : Ordinal.{u_1}} :

Cardinal.aleph0 ≤ Cardinal.aleph' o ↔ Ordinal.omega0 ≤ o

source

@[deprecated Cardinal.preAleph_pos]

theorem Cardinal.aleph'_pos {o : Ordinal.{u_1}} (ho : 0 < o) :

0 < Cardinal.aleph' o

source

@[deprecated Cardinal.preAleph_isNormal]

theorem Cardinal.aleph'_isNormal :

Ordinal.IsNormal (Cardinal.ord ∘ ⇑Cardinal.aleph')

source

@[deprecated]

theorem Cardinal.ord_card_unbounded :

Set.Unbounded (fun (x1 x2 : Ordinal.{u_1}) => x1 < x2) {b : Ordinal.{u_1} | b.card.ord = b}

Ordinals that are cardinals are unbounded.

source

@[deprecated]

theorem Cardinal.eq_aleph'_of_eq_card_ord {o : Ordinal.{u_1}} (ho : o.card.ord = o) :

∃ (a : Ordinal.{u_1}), (Cardinal.aleph' a).ord = o

source

@[deprecated]

theorem Cardinal.ord_card_unbounded' :

Set.Unbounded (fun (x1 x2 : Ordinal.{u_1}) => x1 < x2) {b : Ordinal.{u_1} | b.card.ord = b ∧ Ordinal.omega0 ≤ b}

Infinite ordinals that are cardinals are unbounded.

source

@[deprecated]

theorem Cardinal.eq_aleph_of_eq_card_ord {o : Ordinal.{u_1}} (ho : o.card.ord = o) (ho' : Ordinal.omega0 ≤ o) :

∃ (a : Ordinal.{u_1}), (Cardinal.aleph a).ord = o

Beth cardinals #

source

def Cardinal.beth (o : Ordinal.{u}) :

Cardinal.{u}

Beth numbers are defined so that beth 0 = ℵ₀, beth (succ o) = 2 ^ beth o, and when o is a limit ordinal, beth o is the supremum of beth o' for o' < o.

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, beth o = aleph o for every o.

Equations

One or more equations did not get rendered due to their size.

source

def Cardinal.termℶ_ :

Lean.ParserDescr

Beth numbers are defined so that beth 0 = ℵ₀, beth (succ o) = 2 ^ beth o, and when o is a limit ordinal, beth o is the supremum of beth o' for o' < o.

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, beth o = aleph o for every o.

Equations