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

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)

Instances For

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 b : Ordinal.{u_1}} (ha : a.IsInitial) :
a.card ≤ b.card ↔ a ≤ b
source
theorem Ordinal.IsInitial.card_lt_card {a 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
@[simp]
theorem Ordinal.isInitial_natCast (n : ℕ) :
(↑n).IsInitial
source
theorem Ordinal.isInitial_zero :
IsInitial 0
source
theorem Ordinal.isInitial_one :
IsInitial 1
source
theorem Ordinal.isInitial_omega0 :
omega0.IsInitial
source
theorem Ordinal.isInitial_succ {o : Ordinal.{u_1}} :
(Order.succ o).IsInitial ↔ o < omega0
source
theorem Ordinal.not_bddAbove_isInitial :
¬BddAbove {x : Ordinal.{u_1} | x.IsInitial}
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.

Instances For

source
@[simp]
theorem Ordinal.isInitialIso_symm_apply_coe (x : Cardinal.{u_1}) :
↑((RelIso.symm isInitialIso) x) = x.ord
source
@[simp]
theorem Ordinal.isInitialIso_apply (x : { x : Ordinal.{u_1} // x.IsInitial }) :
isInitialIso x = (↑x).card
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.7} | x.IsInitial}, inj' := Ordinal.preOmega._proof_1, map_rel_iff' := @Ordinal.preOmega._proof_2 }

Instances For

source
theorem Ordinal.coe_preOmega :
⇑preOmega = enumOrd {x : Ordinal.{u_1} | x.IsInitial}
source
theorem Ordinal.preOmega_strictMono :
StrictMono ⇑preOmega
source
theorem Ordinal.preOmega_lt_preOmega {o₁ o₂ : Ordinal.{u_1}} :
preOmega o₁ < preOmega o₂ ↔ o₁ < o₂
source
theorem Ordinal.preOmega_le_preOmega {o₁ o₂ : Ordinal.{u_1}} :
preOmega o₁ ≤ preOmega o₂ ↔ o₁ ≤ o₂
source
theorem Ordinal.preOmega_max (o₁ o₂ : Ordinal.{u_1}) :
preOmega (max o₁ o₂) = max (preOmega o₁) (preOmega o₂)
source
theorem Ordinal.isInitial_preOmega (o : Ordinal.{u_1}) :
(preOmega o).IsInitial
source
theorem Ordinal.le_preOmega_self (o : Ordinal.{u_1}) :
o ≤ preOmega o
source
@[simp]
theorem Ordinal.preOmega_zero :
preOmega 0 = 0
source
@[simp]
theorem Ordinal.preOmega_natCast (n : ℕ) :
preOmega ↑n = ↑n
source
@[simp]
theorem Ordinal.preOmega_ofNat (n : ℕ) [n.AtLeastTwo] :
preOmega (OfNat.ofNat n) = ↑n
source
theorem Ordinal.preOmega_le_of_forall_lt {o a : Ordinal.{u_1}} (ha : a.IsInitial) (H : ∀ b < o, preOmega b < a) :
preOmega o ≤ a
source
theorem Ordinal.isNormal_preOmega :
IsNormal ⇑preOmega
source
@[simp]
theorem Ordinal.range_preOmega :
Set.range ⇑preOmega = {x : Ordinal.{u_1} | x.IsInitial}
source
theorem Ordinal.mem_range_preOmega_iff {x : Ordinal.{u_1}} :
x ∈ Set.range ⇑preOmega ↔ x.IsInitial
source
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`.

source
@[simp]
theorem Ordinal.preOmega_omega0 :
preOmega omega0 = omega0
source
@[simp]
theorem Ordinal.omega0_le_preOmega_iff {x : Ordinal.{u_1}} :
omega0 ≤ preOmega x ↔ omega0 ≤ x
source
@[simp]
theorem Ordinal.omega0_lt_preOmega_iff {x : Ordinal.{u_1}} :
omega0 < preOmega x ↔ 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

Instances For

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

Instances For

source
def Ordinal.termω₁ :
Lean.ParserDescr

`ω₁` is the first uncountable ordinal.

Equations

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

Instances For

source
theorem Ordinal.omega_eq_preOmega (o : Ordinal.{u_1}) :
omega o = preOmega (omega0 + o)
source
theorem Ordinal.omega_strictMono :
StrictMono ⇑omega
source
theorem Ordinal.omega_lt_omega {o₁ o₂ : Ordinal.{u_1}} :
omega o₁ < omega o₂ ↔ o₁ < o₂
source
theorem Ordinal.omega_le_omega {o₁ o₂ : Ordinal.{u_1}} :
omega o₁ ≤ omega o₂ ↔ o₁ ≤ o₂
source
theorem Ordinal.omega_max (o₁ o₂ : Ordinal.{u_1}) :
omega (max o₁ o₂) = max (omega o₁) (omega o₂)
source
theorem Ordinal.preOmega_le_omega (o : Ordinal.{u_1}) :
preOmega o ≤ omega o
source
theorem Ordinal.isInitial_omega (o : Ordinal.{u_1}) :
(omega o).IsInitial
source
theorem Ordinal.le_omega_self (o : Ordinal.{u_1}) :
o ≤ omega o
source
@[simp]
theorem Ordinal.omega_zero :
omega 0 = omega0
source
theorem Ordinal.omega0_le_omega (o : Ordinal.{u_1}) :
omega0 ≤ omega o
source
theorem Ordinal.omega_pos (o : Ordinal.{u_1}) :
0 < omega o

For the theorem `0 < ω`, see `omega0_pos`.

source
theorem Ordinal.omega0_lt_omega1 :
omega0 < omega 1
source
theorem Ordinal.isNormal_omega :
IsNormal ⇑omega
source
@[simp]
theorem Ordinal.range_omega :
Set.range ⇑omega = {x : Ordinal.{u_1} | omega0 ≤ x ∧ x.IsInitial}
source
theorem Ordinal.mem_range_omega_iff {x : Ordinal.{u_1}} :
x ∈ Set.range ⇑omega ↔ 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 = (Ordinal.enumOrdOrderIso {x : Ordinal.{?u.4} | x.IsInitial} Ordinal.not_bddAbove_isInitial).trans Ordinal.isInitialIso

Instances For

source
@[simp]
theorem Ordinal.card_preOmega (o : Ordinal.{u_1}) :
(preOmega o).card = Cardinal.preAleph o
source
@[simp]
theorem Cardinal.ord_preAleph (o : Ordinal.{u_1}) :
(preAleph o).ord = Ordinal.preOmega o
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 :
mk Cardinal.{u} = univ.{u, u + 1}
source
theorem Cardinal.preAleph_lt_preAleph {o₁ o₂ : Ordinal.{u_1}} :
preAleph o₁ < preAleph o₂ ↔ o₁ < o₂
source
theorem Cardinal.preAleph_le_preAleph {o₁ o₂ : Ordinal.{u_1}} :
preAleph o₁ ≤ preAleph o₂ ↔ o₁ ≤ o₂
source
theorem Cardinal.preAleph_max (o₁ o₂ : Ordinal.{u_1}) :
preAleph (max o₁ o₂) = max (preAleph o₁) (preAleph o₂)
source
@[simp]
theorem Cardinal.preAleph_zero :
preAleph 0 = 0
source
@[simp]
theorem Cardinal.preAleph_succ (o : Ordinal.{u_1}) :
preAleph (Order.succ o) = Order.succ (preAleph o)
source
@[simp]
theorem Cardinal.preAleph_nat (n : ℕ) :
preAleph ↑n = ↑n
source
@[simp]
theorem Cardinal.preAleph_omega0 :
preAleph Ordinal.omega0 = aleph0
source
@[simp]
theorem Cardinal.preAleph_pos {o : Ordinal.{u_1}} :
0 < preAleph o ↔ 0 < o
source
@[simp]
theorem Cardinal.aleph0_le_preAleph {o : Ordinal.{u_1}} :
aleph0 ≤ preAleph o ↔ Ordinal.omega0 ≤ o
source
@[simp]
theorem Cardinal.lift_preAleph (o : Ordinal.{u}) :
lift.{v, u} (preAleph o) = preAleph (Ordinal.lift.{v, u} o)
source
@[simp]
theorem Ordinal.lift_preOmega (o : Ordinal.{u}) :
lift.{v, u} (preOmega o) = preOmega (lift.{v, u} o)
source
theorem Cardinal.isNormal_preAleph :
Order.IsNormal ⇑preAleph
source
theorem Cardinal.preAleph_le_of_isSuccPrelimit {o : Ordinal.{u_1}} (l : Order.IsSuccPrelimit o) {c : Cardinal.{u_1}} :
preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c
source
@[deprecated Cardinal.preAleph_le_of_isSuccPrelimit (since := "2025-07-08")]
theorem Cardinal.preAleph_le_of_isLimit {o : Ordinal.{u_1}} (l : Order.IsSuccPrelimit o) {c : Cardinal.{u_1}} :
preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c

Alias of `Cardinal.preAleph_le_of_isSuccPrelimit`.

source
theorem Cardinal.preAleph_limit {o : Ordinal.{u_1}} (ho : Order.IsSuccPrelimit o) :
preAleph o = ⨆ (a : ↑(Set.Iio o)), preAleph ↑a
source
theorem Cardinal.preAleph_le_of_strictMono {f : Ordinal.{u_1} → Cardinal.{u_1}} (hf : StrictMono f) (o : Ordinal.{u_1}) :
preAleph o ≤ f 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.preAleph`.

Equations

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

Instances For

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

Equations

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

Instances For

source
def Cardinal.termℵ₁ :
Lean.ParserDescr

`ℵ₁` is the first uncountable cardinal.

Equations

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

Instances For

source
theorem Cardinal.aleph_eq_preAleph (o : Ordinal.{u_1}) :
aleph o = preAleph (Ordinal.omega0 + o)
source
@[simp]
theorem Ordinal.card_omega (o : Ordinal.{u_1}) :
(omega o).card = Cardinal.aleph o
source
@[simp]
theorem Cardinal.ord_aleph (o : Ordinal.{u_1}) :
(aleph o).ord = Ordinal.omega o
source
theorem Cardinal.aleph_lt_aleph {o₁ o₂ : Ordinal.{u_1}} :
aleph o₁ < aleph o₂ ↔ o₁ < o₂
source
theorem Cardinal.aleph_le_aleph {o₁ o₂ : Ordinal.{u_1}} :
aleph o₁ ≤ aleph o₂ ↔ o₁ ≤ o₂
source
theorem Cardinal.aleph_max (o₁ o₂ : Ordinal.{u_1}) :
aleph (max o₁ o₂) = max (aleph o₁) (aleph o₂)
source
theorem Cardinal.preAleph_le_aleph (o : Ordinal.{u_1}) :
preAleph o ≤ aleph o
source
@[simp]
theorem Cardinal.aleph_succ (o : Ordinal.{u_1}) :
aleph (Order.succ o) = Order.succ (aleph o)
source
@[simp]
theorem Cardinal.aleph_zero :
aleph 0 = aleph0
source
@[simp]
theorem Cardinal.lift_aleph (o : Ordinal.{u}) :
lift.{v, u} (aleph o) = aleph (Ordinal.lift.{v, u} o)
source
@[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`.

source
theorem Cardinal.isNormal_aleph :
Order.IsNormal ⇑aleph
source
theorem Cardinal.aleph_limit {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) :
aleph o = ⨆ (a : ↑(Set.Iio o)), aleph ↑a
source
theorem Cardinal.aleph0_le_aleph (o : Ordinal.{u_1}) :
aleph0 ≤ aleph o
source
theorem Cardinal.aleph_pos (o : Ordinal.{u_1}) :
0 < aleph o
source
@[simp]
theorem Cardinal.aleph_toNat (o : Ordinal.{u_1}) :
toNat (aleph o) = 0
source
@[simp]
theorem Cardinal.aleph_toENat (o : Ordinal.{u_1}) :
toENat (aleph o) = ⊤
source
theorem Cardinal.isSuccLimit_omega (o : Ordinal.{u_1}) :
Order.IsSuccLimit (Ordinal.omega o)
source
@[deprecated Cardinal.isSuccLimit_omega (since := "2025-07-08")]
theorem Cardinal.isLimit_omega (o : Ordinal.{u_1}) :
Order.IsSuccLimit (Ordinal.omega o)

Alias of `Cardinal.isSuccLimit_omega`.

source
@[simp]
theorem Cardinal.range_aleph :
Set.range ⇑aleph = Set.Ici aleph0
source
theorem Cardinal.mem_range_aleph_iff {c : Cardinal.{u_1}} :
c ∈ Set.range ⇑aleph ↔ aleph0 ≤ c
source
@[simp]
theorem Cardinal.succ_aleph0 :
Order.succ aleph0 = aleph 1
source
theorem Cardinal.aleph0_lt_aleph_one :
aleph0 < aleph 1
source
theorem Cardinal.countable_iff_lt_aleph_one {α : Type u_1} (s : Set α) :
s.Countable ↔ mk ↑s < aleph 1
source
@[simp]
theorem Cardinal.aleph1_le_lift {c : Cardinal.{u}} :
aleph 1 ≤ lift.{v, u} c ↔ aleph 1 ≤ c
source
@[simp]
theorem Cardinal.lift_le_aleph1 {c : Cardinal.{u}} :
lift.{v, u} c ≤ aleph 1 ↔ c ≤ aleph 1
source
@[simp]
theorem Cardinal.aleph1_lt_lift {c : Cardinal.{u}} :
aleph 1 < lift.{v, u} c ↔ aleph 1 < c
source
@[simp]
theorem Cardinal.lift_lt_aleph1 {c : Cardinal.{u}} :
lift.{v, u} c < aleph 1 ↔ c < aleph 1
source
@[simp]
theorem Cardinal.aleph1_eq_lift {c : Cardinal.{u}} :
aleph 1 = lift.{v, u} c ↔ aleph 1 = c
source
@[simp]
theorem Cardinal.lift_eq_aleph1 {c : Cardinal.{u}} :
lift.{v, u} c = aleph 1 ↔ c = aleph 1
source
theorem Cardinal.lt_omega_iff_card_lt {x o : Ordinal.{u_1}} :
x < Ordinal.omega o ↔ x.card < aleph o

### Beth cardinals #

source
@[irreducible]
def Cardinal.preBeth (o : Ordinal.{u}) :
Cardinal.{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

Instances For

source
theorem Cardinal.preBeth_strictMono :
StrictMono preBeth
source
theorem Cardinal.preBeth_mono :
Monotone preBeth
source
theorem Cardinal.preAleph_le_preBeth (o : Ordinal.{u_1}) :
preAleph o ≤ preBeth o
source
@[simp]
theorem Cardinal.preBeth_lt_preBeth {o₁ o₂ : Ordinal.{u_1}} :
preBeth o₁ < preBeth o₂ ↔ o₁ < o₂
source
@[simp]
theorem Cardinal.preBeth_le_preBeth {o₁ o₂ : Ordinal.{u_1}} :
preBeth o₁ ≤ preBeth o₂ ↔ o₁ ≤ o₂
source
@[simp]
theorem Cardinal.preBeth_inj {o₁ o₂ : Ordinal.{u_1}} :
preBeth o₁ = preBeth o₂ ↔ o₁ = o₂
source
@[simp]
theorem Cardinal.preBeth_zero :
preBeth 0 = 0
source
@[simp]
theorem Cardinal.preBeth_succ (o : Ordinal.{u_1}) :
preBeth (Order.succ o) = 2 ^ preBeth o
source
theorem Cardinal.preBeth_limit {o : Ordinal.{u_1}} (ho : Order.IsSuccPrelimit o) :
preBeth o = ⨆ (a : ↑(Set.Iio o)), preBeth ↑a
source
theorem Cardinal.isNormal_preBeth :
Order.IsNormal preBeth
source
theorem Cardinal.preBeth_nat (n : ℕ) :
preBeth ↑n = ↑((fun (x : ℕ) => 2 ^ x)^[n] 0)
source
@[simp]
theorem Cardinal.preBeth_one :
preBeth 1 = 1
source
@[simp]
theorem Cardinal.preBeth_omega :
preBeth Ordinal.omega0 = aleph0
source
@[simp]
theorem Cardinal.preBeth_pos {o : Ordinal.{u_1}} :
0 < preBeth o ↔ 0 < o
source
@[simp]
theorem Cardinal.preBeth_eq_zero {o : Ordinal.{u_1}} :
preBeth o = 0 ↔ o = 0
source
theorem Cardinal.isStrongLimit_preBeth {o : Ordinal.{u_1}} :
(preBeth o).IsStrongLimit ↔ Order.IsSuccLimit o
source
def Cardinal.beth (o : Ordinal.{u}) :
Cardinal.{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)

Instances For

source
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 "ℶ_ ")

Instances For

source
theorem Cardinal.beth_eq_preBeth (o : Ordinal.{u_1}) :
beth o = preBeth (Ordinal.omega0 + o)
source
theorem Cardinal.preBeth_le_beth (o : Ordinal.{u_1}) :
preBeth o ≤ beth o
source
theorem Cardinal.beth_strictMono :
StrictMono beth
source
theorem Cardinal.beth_mono :
Monotone beth
source
@[simp]
theorem Cardinal.beth_lt_beth {o₁ o₂ : Ordinal.{u_1}} :
beth o₁ < beth o₂ ↔ o₁ < o₂
source
@[simp]
theorem Cardinal.beth_le_beth {o₁ o₂ : Ordinal.{u_1}} :
beth o₁ ≤ beth o₂ ↔ o₁ ≤ o₂
source
@[simp]
theorem Cardinal.beth_zero :
beth 0 = aleph0
source
@[simp]
theorem Cardinal.beth_succ (o : Ordinal.{u_1}) :
beth (Order.succ o) = 2 ^ beth o
source
theorem Cardinal.isNormal_beth :
Order.IsNormal beth
source
theorem Cardinal.beth_limit {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) :
beth o = ⨆ (a : ↑(Set.Iio o)), beth ↑a
source
theorem Cardinal.aleph_le_beth (o : Ordinal.{u_1}) :
aleph o ≤ beth o
source
theorem Cardinal.aleph0_le_beth (o : Ordinal.{u_1}) :
aleph0 ≤ beth o
source
theorem Cardinal.beth_pos (o : Ordinal.{u_1}) :
0 < beth o
source
theorem Cardinal.beth_ne_zero (o : Ordinal.{u_1}) :
beth o ≠ 0
source
theorem Cardinal.isStrongLimit_beth {o : Ordinal.{u_1}} :
(beth o).IsStrongLimit ↔ Order.IsSuccPrelimit o