Documentation

Mathlib.SetTheory.Cardinal.Aleph

Omega, aleph, and beth functions #

This file defines the ω, ℵ, and ℶ functions which enumerate certain kinds of ordinals and cardinals. Each is provided in two variants: the standard versions which only take infinite values, and "preliminary" versions which include finite values and are sometimes more convenient.

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 cardinals.
The function Cardinal.preBeth is the unique normal function with beth 0 = 0 and beth (succ o) = 2 ^ beth o. Cardinal.beth is the more standard function which skips over finite cardinals.

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

Omega ordinals #

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

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)

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

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

a.card ≤ b.card ↔ a ≤ b

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

a.card < b.card ↔ a < b

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

c.ord.IsInitial

theorem Ordinal.isInitial_natCast (n : ℕ) :

(↑n).IsInitial

theorem Ordinal.isInitial_zero :

theorem Ordinal.isInitial_one :

theorem Ordinal.isInitial_omega0 :

omega0.IsInitial

theorem Ordinal.not_bddAbove_isInitial :

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

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.

@[simp]

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

isInitialIso x = (↑x).card

@[simp]

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

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

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.7} | x.IsInitial}, inj' := Ordinal.preOmega._proof_1, map_rel_iff' := @Ordinal.preOmega._proof_2 }

theorem Ordinal.coe_preOmega :

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

theorem Ordinal.preOmega_strictMono :

StrictMono ⇑preOmega

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

preOmega o₁ < preOmega o₂ ↔ o₁ < o₂

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

preOmega o₁ ≤ preOmega o₂ ↔ o₁ ≤ o₂

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

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

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

(preOmega o).IsInitial

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

o ≤ preOmega o

@[simp]

theorem Ordinal.preOmega_zero :

@[simp]

theorem Ordinal.preOmega_natCast (n : ℕ) :

preOmega ↑n = ↑n

@[simp]

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

preOmega (OfNat.ofNat n) = ↑n

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

preOmega o ≤ a

theorem Ordinal.isNormal_preOmega :

IsNormal ⇑preOmega

@[simp]

theorem Ordinal.range_preOmega :

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

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

x ∈ Set.range ⇑preOmega ↔ x.IsInitial

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

x.IsInitial → x ∈ Set.range ⇑preOmega

Alias of the reverse direction of Ordinal.mem_range_preOmega_iff.

@[simp]

theorem Ordinal.preOmega_omega0 :

preOmega omega0 = omega0

@[simp]

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

omega0 ≤ preOmega x ↔ omega0 ≤ x

@[simp]

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

omega0 < preOmega x ↔ omega0 < x

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

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 "ω_ ")

def Ordinal.termω₁ :

Lean.ParserDescr

ω₁ is the first uncountable ordinal.

Equations

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

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

omega o = preOmega (omega0 + o)

theorem Ordinal.omega_strictMono :

StrictMono ⇑omega

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

omega o₁ < omega o₂ ↔ o₁ < o₂

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

omega o₁ ≤ omega o₂ ↔ o₁ ≤ o₂

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

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

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

preOmega o ≤ omega o

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

(omega o).IsInitial

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

@[simp]

theorem Ordinal.omega_zero :

omega 0 = omega0

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

omega0 ≤ omega o

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

For the theorem 0 < ω, see omega0_pos.

theorem Ordinal.omega0_lt_omega1 :

omega0 < omega 1

theorem Ordinal.isNormal_omega :

IsNormal ⇑omega

@[simp]

theorem Ordinal.range_omega :

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

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

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

Aleph cardinals #

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 = (Ordinal.enumOrdOrderIso {x : Ordinal.{?u.4} | x.IsInitial} Ordinal.not_bddAbove_isInitial).trans Ordinal.isInitialIso

@[simp]

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

(preOmega o).card = Cardinal.preAleph o

@[simp]

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

(preAleph o).ord = Ordinal.preOmega o

@[simp]

theorem Cardinal.type_cardinal :

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

@[simp]

theorem Cardinal.mk_cardinal :

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

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

preAleph o₁ < preAleph o₂ ↔ o₁ < o₂

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

preAleph o₁ ≤ preAleph o₂ ↔ o₁ ≤ o₂

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

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

@[simp]

theorem Cardinal.preAleph_zero :

@[simp]

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

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

@[simp]

theorem Cardinal.preAleph_nat (n : ℕ) :

preAleph ↑n = ↑n

@[simp]

theorem Cardinal.preAleph_omega0 :

preAleph Ordinal.omega0 = aleph0

@[simp]

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

0 < preAleph o ↔ 0 < o

@[simp]

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

aleph0 ≤ preAleph o ↔ Ordinal.omega0 ≤ o

@[simp]

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

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

@[simp]

theorem Ordinal.lift_preOmega (o : Ordinal.{u}) :

lift.{v, u} (preOmega o) = preOmega (lift.{v, u} o)

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

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

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

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

theorem Cardinal.preAleph_le_of_strictMono {f : Ordinal.{u_1} → Cardinal.{u_1}} (hf : StrictMono f) (o : Ordinal.{u_1}) :

preAleph o ≤ f o

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

Equations

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

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

Equations

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

def Cardinal.termℵ₁ :

Lean.ParserDescr

ℵ₁ is the first uncountable cardinal.

Equations

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

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

aleph o = preAleph (Ordinal.omega0 + o)

@[simp]

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

(omega o).card = Cardinal.aleph o

@[simp]

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

(aleph o).ord = Ordinal.omega o

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

aleph o₁ < aleph o₂ ↔ o₁ < o₂

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

aleph o₁ ≤ aleph o₂ ↔ o₁ ≤ o₂

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

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

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

preAleph o ≤ aleph o

@[simp]

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

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

@[simp]

theorem Cardinal.aleph_zero :

aleph 0 = aleph0

@[simp]

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

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

@[simp]

theorem Ordinal.lift_omega (o : Ordinal.{u}) :

lift.{v, u} (omega o) = omega (lift.{v, u} o)

For the theorem lift ω = ω, see lift_omega0.

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

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

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

aleph0 ≤ aleph o

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

@[simp]

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

toNat (aleph o) = 0

@[simp]

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

toENat (aleph o) = ⊤

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

(Ordinal.omega o).IsLimit

@[simp]

theorem Cardinal.range_aleph :

Set.range ⇑aleph = Set.Ici aleph0

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

c ∈ Set.range ⇑aleph ↔ aleph0 ≤ c

@[simp]

theorem Cardinal.succ_aleph0 :

Order.succ aleph0 = aleph 1

theorem Cardinal.aleph0_lt_aleph_one :

aleph0 < aleph 1

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

s.Countable ↔ mk ↑s < aleph 1

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

theorem Cardinal.lt_omega_iff_card_lt {x o : Ordinal.{u_1}} :

x < Ordinal.omega o ↔ x.card < aleph o

Beth cardinals #

@[irreducible]

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

The "pre-beth" function is defined so that preBeth o is the supremum of 2 ^ preBeth a for a < o. This implies beth 0 = 0, beth (succ o) = 2 ^ beth o, and that for a limit ordinal o, beth o is the supremum of beth a for a < o.

For the usual function starting at ℵ₀, see Cardinal.beth.

Equations

Cardinal.preBeth o = ⨆ (a : ↑(Set.Iio o)), 2 ^ Cardinal.preBeth ↑a

theorem Cardinal.preBeth_strictMono :

StrictMono preBeth

theorem Cardinal.preBeth_mono :

Monotone preBeth

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

preAleph o ≤ preBeth o

@[simp]

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

preBeth o₁ < preBeth o₂ ↔ o₁ < o₂

@[simp]

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

preBeth o₁ ≤ preBeth o₂ ↔ o₁ ≤ o₂

@[simp]

theorem Cardinal.preBeth_zero :

@[simp]

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

preBeth (Order.succ o) = 2 ^ preBeth o

theorem Cardinal.preBeth_limit {o : Ordinal.{u_1}} (ho : Order.IsSuccPrelimit o) :

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

theorem Cardinal.preBeth_nat (n : ℕ) :

preBeth ↑n = ↑((fun (x : ℕ) => 2 ^ x)^[n] 0)

@[simp]

theorem Cardinal.preBeth_one :

@[simp]

theorem Cardinal.preBeth_omega :

preBeth Ordinal.omega0 = aleph0

@[simp]

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

0 < preBeth o ↔ 0 < o

theorem Cardinal.isNormal_preBeth :

Ordinal.IsNormal (ord ∘ preBeth)

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

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

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have ℶ_ o = ℵ_ o for all ordinals.

For a version which starts at zero, see Cardinal.preBeth.

Equations

Cardinal.beth o = Cardinal.preBeth (Ordinal.omega0 + o)

def Cardinal.termℶ_ :

Lean.ParserDescr

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

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have ℶ_ o = ℵ_ o for all ordinals.

For a version which starts at zero, see Cardinal.preBeth.

Equations

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

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

beth o = preBeth (Ordinal.omega0 + o)

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

preBeth o ≤ beth o

theorem Cardinal.beth_strictMono :

StrictMono beth

theorem Cardinal.beth_mono :

@[simp]

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

beth o₁ < beth o₂ ↔ o₁ < o₂

@[deprecated Cardinal.beth_lt_beth (since := "2025-01-14")]

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

beth o₁ < beth o₂ ↔ o₁ < o₂

Alias of Cardinal.beth_lt_beth.

@[simp]

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

beth o₁ ≤ beth o₂ ↔ o₁ ≤ o₂

@[deprecated Cardinal.beth_le_beth (since := "2025-01-14")]

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

beth o₁ ≤ beth o₂ ↔ o₁ ≤ o₂

Alias of Cardinal.beth_le_beth.

@[simp]

theorem Cardinal.beth_zero :

beth 0 = aleph0

@[simp]

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

beth (Order.succ o) = 2 ^ beth o

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

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

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

aleph o ≤ beth o

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

aleph0 ≤ beth o

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

0 < beth o

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

theorem Cardinal.isNormal_beth :

Ordinal.IsNormal (ord ∘ beth)

theorem Cardinal.isStrongLimit_beth {o : Ordinal.{u_1}} (H : Order.IsSuccPrelimit o) :

(beth o).IsStrongLimit