Mathlib.SetTheory.Cardinal.Aleph

Ordinal.IsInitial definition

(o : Ordinal) : Prop

Full source

/-- 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`. -/
def IsInitial (o : Ordinal) : Prop :=
  o.card.ord = o

Initial ordinal

Informal description

An ordinal $o$ is called *initial* if it is the smallest ordinal with its cardinality, i.e., $o = \text{ord}(\text{card}(o))$, where $\text{card}(o)$ denotes the cardinality of $o$ and $\text{ord}(\kappa)$ denotes the smallest ordinal with cardinality $\kappa$.

Ordinal.IsInitial.ord_card theorem

{o : Ordinal} (h : IsInitial o) : o.card.ord = o

Full source

theorem IsInitial.ord_card {o : Ordinal} (h : IsInitial o) : o.card.ord = o := h

Initial Ordinal Cardinality Identity: $\text{ord}(\text{card}(o)) = o$

Informal description

For any initial ordinal $o$, the smallest ordinal with the same cardinality as $o$ is $o$ itself, i.e., $\text{ord}(\text{card}(o)) = o$.

Ordinal.IsInitial.card_le_card theorem

{a b : Ordinal} (ha : IsInitial a) : a.card ≤ b.card ↔ a ≤ b

Full source

theorem IsInitial.card_le_card {a b : Ordinal} (ha : IsInitial a) : a.card ≤ b.card ↔ a ≤ b := by
  refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩
  rw [← ord_le_ord, ha.ord_card] at h
  exact h.trans (ord_card_le b)

Cardinality Comparison for Initial Ordinals: $\text{card}(a) \leq \text{card}(b) \leftrightarrow a \leq b$

Informal description

For any ordinals $a$ and $b$, if $a$ is initial, then the cardinality of $a$ is less than or equal to the cardinality of $b$ if and only if $a$ is less than or equal to $b$. In symbols: $$ \text{card}(a) \leq \text{card}(b) \leftrightarrow a \leq b $$

Ordinal.IsInitial.card_lt_card theorem

{a b : Ordinal} (hb : IsInitial b) : a.card < b.card ↔ a < b

Full source

theorem IsInitial.card_lt_card {a b : Ordinal} (hb : IsInitial b) : a.card < b.card ↔ a < b :=
  lt_iff_lt_of_le_iff_le hb.card_le_card

Strict Cardinality Comparison for Initial Ordinals: $\text{card}(a) < \text{card}(b) \leftrightarrow a < b$

Informal description

For any ordinals $a$ and $b$, if $b$ is initial, then the cardinality of $a$ is strictly less than the cardinality of $b$ if and only if $a$ is strictly less than $b$. In symbols: $$ \text{card}(a) < \text{card}(b) \leftrightarrow a < b $$

Ordinal.isInitial_ord theorem

(c : Cardinal) : IsInitial c.ord

Full source

theorem isInitial_ord (c : Cardinal) : IsInitial c.ord := by
  rw [IsInitial, card_ord]

Initiality of the smallest ordinal with given cardinality

Informal description

For any cardinal number $c$, the ordinal $\mathrm{ord}(c)$ (the smallest ordinal with cardinality $c$) is initial. That is, $\mathrm{ord}(c)$ is the smallest ordinal whose cardinality is $c$.

Ordinal.isInitial_natCast theorem

(n : ℕ) : IsInitial n

Full source

theorem isInitial_natCast (n : ℕ) : IsInitial n := by
  rw [IsInitial, card_nat, ord_nat]

Initiality of Finite Ordinals: $n$ is initial for all $n \in \mathbb{N}$

Informal description

For any natural number $n$, the ordinal $n$ is initial, meaning it is the smallest ordinal with its cardinality.

Ordinal.isInitial_zero theorem

: IsInitial 0

Full source

theorem isInitial_zero : IsInitial 0 := by
  exact_mod_cast isInitial_natCast 0

Initiality of Zero Ordinal: $0$ is initial

Informal description

The ordinal $0$ is initial, meaning it is the smallest ordinal with its cardinality (which is $0$).

Ordinal.isInitial_one theorem

: IsInitial 1

Full source

theorem isInitial_one : IsInitial 1 := by
  exact_mod_cast isInitial_natCast 1

Initiality of the Ordinal One

Informal description

The ordinal $1$ is initial, meaning it is the smallest ordinal with its cardinality.

Ordinal.isInitial_omega0 theorem

: IsInitial ω

Full source

theorem isInitial_omega0 : IsInitial ω := by
  rw [IsInitial, card_omega0, ord_aleph0]

$\omega$ is an initial ordinal

Informal description

The ordinal $\omega$ (the smallest infinite ordinal) is initial, meaning it is the smallest ordinal with its cardinality $\aleph_0$.

Ordinal.not_bddAbove_isInitial theorem

: ¬BddAbove {x | IsInitial x}

Full source

theorem not_bddAbove_isInitial : ¬ BddAbove {x | IsInitial x} := by
  rintro ⟨a, ha⟩
  have := ha (isInitial_ord (succ a.card))
  rw [ord_le] at this
  exact (lt_succ _).not_le this

Unboundedness of Initial Ordinals

Informal description

The set of initial ordinals is not bounded above. That is, for any ordinal $\alpha$, there exists an initial ordinal $\beta$ such that $\alpha < \beta$.

Ordinal.isInitialIso definition

: { x // IsInitial x } ≃o Cardinal

Full source

/-- Initial ordinals are order-isomorphic to the cardinals. -/
@[simps!]
def isInitialIso : {x // IsInitial x}{x // IsInitial x} ≃o Cardinal where
  toFun x := x.1.card
  invFun x := ⟨x.ord, isInitial_ord _⟩
  left_inv x := Subtype.ext x.2.ord_card
  right_inv x := card_ord x
  map_rel_iff' {a _} := a.2.card_le_card

Order isomorphism between initial ordinals and cardinals

Informal description

The order isomorphism between the subtype of initial ordinals (ordinals that are the smallest with their cardinality) and the type of cardinal numbers. Specifically: - The forward map sends an initial ordinal $x$ to its cardinality $\mathrm{card}(x)$. - The inverse map sends a cardinal $\kappa$ to the smallest ordinal $\mathrm{ord}(\kappa)$ with cardinality $\kappa$. - The isomorphism preserves the order relation: for initial ordinals $a$ and $b$, we have $a \leq b$ if and only if $\mathrm{card}(a) \leq \mathrm{card}(b)$.

Ordinal.preOmega definition

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

Full source

/-- 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`. -/
def preOmega : OrdinalOrdinal.{u}Ordinal.{u} ↪o Ordinal.{u} where
  toFun := enumOrd {x | IsInitial x}
  inj' _ _ h := enumOrd_injective not_bddAbove_isInitial h
  map_rel_iff' := enumOrd_le_enumOrd not_bddAbove_isInitial

Pre-omega function (enumeration of initial ordinals)

Informal description

The "pre-omega" function is an order embedding from ordinals to ordinals that enumerates the initial ordinals. For any ordinal index $o$, the value $\text{preOmega}(o)$ is the smallest ordinal with its cardinality. Specifically, $\text{preOmega}(n) = n$ for finite ordinals $n$, $\text{preOmega}(\omega) = \omega$, $\text{preOmega}(\omega + 1) = \omega_1$, and so on. This function is defined as the enumeration of the class of all initial ordinals $\{x \mid \text{IsInitial}(x)\}$, where $\text{IsInitial}(x)$ means $x$ is the smallest ordinal with its cardinality. The function is strictly monotonic and injective.

Ordinal.coe_preOmega theorem

: preOmega = enumOrd {x | IsInitial x}

Full source

theorem coe_preOmega : preOmega = enumOrd {x | IsInitial x} :=
  rfl

Pre-omega Function as Enumeration of Initial Ordinals

Informal description

The pre-omega function $\text{preOmega}$ is equal to the enumeration of the class of all initial ordinals $\{x \mid x \text{ is initial}\}$, where an ordinal $x$ is *initial* if it is the smallest ordinal with its cardinality.

Ordinal.preOmega_strictMono theorem

: StrictMono preOmega

Full source

theorem preOmega_strictMono : StrictMono preOmega :=
  preOmega.strictMono

Strict Monotonicity of the Pre-Omega Function

Informal description

The pre-omega function $\text{preOmega} \colon \text{Ordinal} \to \text{Ordinal}$ is strictly monotone, meaning that for any ordinals $o_1$ and $o_2$, if $o_1 < o_2$ then $\text{preOmega}(o_1) < \text{preOmega}(o_2)$.

Ordinal.preOmega_lt_preOmega theorem

{o₁ o₂ : Ordinal} : preOmega o₁ < preOmega o₂ ↔ o₁ < o₂

Full source

theorem preOmega_lt_preOmega {o₁ o₂ : Ordinal} : preOmegapreOmega o₁ < preOmega o₂ ↔ o₁ < o₂ :=
  preOmega.lt_iff_lt

Pre-omega Function Preserves Strict Order

Informal description

For any ordinals $o_1$ and $o_2$, the pre-omega function satisfies $\text{preOmega}(o_1) < \text{preOmega}(o_2)$ if and only if $o_1 < o_2$.

Ordinal.preOmega_le_preOmega theorem

{o₁ o₂ : Ordinal} : preOmega o₁ ≤ preOmega o₂ ↔ o₁ ≤ o₂

Full source

theorem preOmega_le_preOmega {o₁ o₂ : Ordinal} : preOmegapreOmega o₁ ≤ preOmega o₂ ↔ o₁ ≤ o₂ :=
  preOmega.le_iff_le

Pre-omega Function Preserves Order Relation

Informal description

For any ordinals $o₁$ and $o₂$, the pre-omega function satisfies $\text{preOmega}(o₁) \leq \text{preOmega}(o₂)$ if and only if $o₁ \leq o₂$.

Ordinal.preOmega_max theorem

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

Full source

theorem preOmega_max (o₁ o₂ : Ordinal) : preOmega (max o₁ o₂) = max (preOmega o₁) (preOmega o₂) :=
  preOmega.monotone.map_max

Pre-omega Function Preserves Maximum Operation on Ordinals

Informal description

For any two ordinals $o₁$ and $o₂$, the pre-omega function satisfies $\text{preOmega}(\max(o₁, o₂)) = \max(\text{preOmega}(o₁), \text{preOmega}(o₂))$.

Ordinal.isInitial_preOmega theorem

(o : Ordinal) : IsInitial (preOmega o)

Full source

theorem isInitial_preOmega (o : Ordinal) : IsInitial (preOmega o) :=
  enumOrd_mem not_bddAbove_isInitial o

Initiality of $\mathrm{preOmega}(o)$ for any ordinal $o$

Informal description

For any ordinal $o$, the ordinal $\mathrm{preOmega}(o)$ is initial, meaning it is the smallest ordinal with its cardinality.

Ordinal.le_preOmega_self theorem

(o : Ordinal) : o ≤ preOmega o

Full source

theorem le_preOmega_self (o : Ordinal) : o ≤ preOmega o :=
  preOmega_strictMono.le_apply

Pre-Omega Function Dominates the Identity on Ordinals

Informal description

For any ordinal $o$, the ordinal $o$ is less than or equal to its image under the pre-omega function, i.e., $o \leq \text{preOmega}(o)$.

Ordinal.preOmega_zero theorem

: preOmega 0 = 0

Full source

@[simp]
theorem preOmega_zero : preOmega 0 = 0 := by
  rw [coe_preOmega, enumOrd_zero]
  exact csInf_eq_bot_of_bot_mem isInitial_zero

Pre-Omega at Zero: $\text{preOmega}(0) = 0$

Informal description

The pre-omega function evaluated at the ordinal $0$ is equal to $0$, i.e., $\text{preOmega}(0) = 0$.

Ordinal.preOmega_natCast theorem

(n : ℕ) : preOmega n = n

Full source

@[simp]
theorem preOmega_natCast (n : ℕ) : preOmega n = n := by
  induction n with
  | zero => exact preOmega_zero
  | succ n IH =>
    apply (le_preOmega_self _).antisymm'
    apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)
    rw [Nat.cast_lt]
    exact lt_succ n

Pre-Omega Function on Natural Numbers: $\text{preOmega}(n) = n$

Informal description

For any natural number $n$, the pre-omega function evaluated at the ordinal $n$ is equal to $n$, i.e., $\text{preOmega}(n) = n$.

Ordinal.preOmega_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : preOmega ofNat(n) = n

Full source

@[simp]
theorem preOmega_ofNat (n : ℕ) [n.AtLeastTwo] : preOmega ofNat(n) = n :=
  preOmega_natCast n

Pre-Omega Function on Numerals: $\text{preOmega}(n) = n$ for $n \geq 2$

Informal description

For any natural number $n \geq 2$, the pre-omega function evaluated at the ordinal corresponding to $n$ (via the `OfNat` instance) equals $n$, i.e., $\text{preOmega}(n) = n$.

Ordinal.preOmega_le_of_forall_lt theorem

{o a : Ordinal} (ha : IsInitial a) (H : ∀ b < o, preOmega b < a) : preOmega o ≤ a

Full source

theorem preOmega_le_of_forall_lt {o a : Ordinal} (ha : IsInitial a) (H : ∀ b < o, preOmega b < a) :
    preOmega o ≤ a :=
  enumOrd_le_of_forall_lt ha H

Upper Bound for preOmega at Limit Ordinals

Informal description

Let $o$ and $a$ be ordinals, where $a$ is initial (i.e., $a$ is the smallest ordinal with its cardinality). If for every ordinal $b < o$, we have $\text{preOmega}(b) < a$, then $\text{preOmega}(o) \leq a$.

Ordinal.isNormal_preOmega theorem

: IsNormal preOmega

Full source

theorem isNormal_preOmega : IsNormal preOmega := by
  rw [isNormal_iff_strictMono_limit]
  refine ⟨preOmega_strictMono, fun o ho a ha ↦
    (preOmega_le_of_forall_lt (isInitial_ord _) fun b hb ↦ ?_).trans (ord_card_le a)⟩
  rw [← (isInitial_ord _).card_lt_card, card_ord]
  apply lt_of_lt_of_le _ (card_le_card <| ha _ (ho.succ_lt hb))
  rw [(isInitial_preOmega _).card_lt_card, preOmega_lt_preOmega]
  exact lt_succ b

Normality of the Pre-Omega Function

Informal description

The pre-omega function $\text{preOmega} \colon \text{Ordinal} \to \text{Ordinal}$ is a normal function. That is: 1. It is strictly increasing: for any ordinals $o_1$ and $o_2$, if $o_1 < o_2$ then $\text{preOmega}(o_1) < \text{preOmega}(o_2)$. 2. It is continuous at limit ordinals: for any limit ordinal $o$ and any increasing sequence $(o_i)_{i < o}$ with supremum $o$, we have $\text{preOmega}(o) = \sup_{i < o} \text{preOmega}(o_i)$.

Ordinal.range_preOmega theorem

: range preOmega = {x | IsInitial x}

Full source

@[simp]
theorem range_preOmega : range preOmega = {x | IsInitial x} :=
  range_enumOrd not_bddAbove_isInitial

Range of preOmega Equals Initial Ordinals

Informal description

The range of the pre-omega function is exactly the set of all initial ordinals. That is, for any ordinal $x$, $x$ is in the range of $\text{preOmega}$ if and only if $x$ is initial (i.e., $x$ is the smallest ordinal with its cardinality).

Ordinal.mem_range_preOmega_iff theorem

{x : Ordinal} : x ∈ range preOmega ↔ IsInitial x

Full source

theorem mem_range_preOmega_iff {x : Ordinal} : x ∈ range preOmegax ∈ range preOmega ↔ IsInitial x := by
  rw [range_preOmega, mem_setOf]

Characterization of Initial Ordinals via Pre-Omega Range: $x \in \text{range}(\text{preOmega}) \leftrightarrow \text{IsInitial}(x)$

Informal description

An ordinal $x$ belongs to the range of the pre-omega function if and only if $x$ is an initial ordinal, i.e., $x$ is the smallest ordinal with its cardinality.

Ordinal.preOmega_omega0 theorem

: preOmega ω = ω

Full source

@[simp]
theorem preOmega_omega0 : preOmega ω = ω := by
  simp_rw [← isNormal_preOmega.apply_omega0, preOmega_natCast, iSup_natCast]

Pre-Omega Function at $\omega$: $\text{preOmega}(\omega) = \omega$

Informal description

The pre-omega function evaluated at the ordinal $\omega$ is equal to $\omega$, i.e., $\text{preOmega}(\omega) = \omega$.

Ordinal.omega0_le_preOmega_iff theorem

{x : Ordinal} : ω ≤ preOmega x ↔ ω ≤ x

Full source

@[simp]
theorem omega0_le_preOmega_iff {x : Ordinal} : ωω ≤ preOmega x ↔ ω ≤ x := by
  conv_lhs => rw [← preOmega_omega0, preOmega_le_preOmega]

Inequality Characterization for Pre-Omega Function: $\omega \leq \text{preOmega}(x) \leftrightarrow \omega \leq x$

Informal description

For any ordinal $x$, the inequality $\omega \leq \text{preOmega}(x)$ holds if and only if $\omega \leq x$.

Ordinal.omega0_lt_preOmega_iff theorem

{x : Ordinal} : ω < preOmega x ↔ ω < x

Full source

@[simp]
theorem omega0_lt_preOmega_iff {x : Ordinal} : ωω < preOmega x ↔ ω < x := by
  conv_lhs => rw [← preOmega_omega0, preOmega_lt_preOmega]

$\omega < \text{preOmega}(x) \leftrightarrow \omega < x$

Informal description

For any ordinal $x$, the inequality $\omega < \text{preOmega}(x)$ holds if and only if $\omega < x$.

Ordinal.omega definition

: Ordinal ↪o Ordinal

Full source

/-- 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`. -/
def omega : OrdinalOrdinal ↪o Ordinal :=
  (OrderEmbedding.addLeft ω).trans preOmega

Omega function (enumeration of infinite initial ordinals)

Informal description

The function `omega` enumerates the infinite initial ordinals indexed by ordinals. Specifically, `omega 0 = ω` (the first infinite ordinal), `omega 1 = ω₁` (the first uncountable ordinal), and so on. This function is an order embedding (strictly monotonic and injective) obtained by composing the order embedding `preOmega` (which enumerates all initial ordinals) with the translation-by-ω embedding. Note that this differs from the first infinite ordinal `Ordinal.omega0` (denoted simply `ω`). For a version that includes finite ordinals, see `Ordinal.preOmega`.

Ordinal.termω_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped notation "ω_ " => omega

Notation for infinite ordinals (ω_)

Informal description

The notation `ω_` is defined as a shorthand for the function `Ordinal.omega`, which enumerates infinite ordinals. Specifically, `ω_ o` represents the `o`-th infinite ordinal, where `ω_ 1` is the first uncountable ordinal (denoted `ω₁` in traditional notation).

Ordinal.termω₁ definition

: Lean.ParserDescr✝

Full source

/-- `ω₁` is the first uncountable ordinal. -/
scoped notation "ω₁" => ω_ 1

First uncountable ordinal (ω₁)

Informal description

The notation `ω₁` represents the first uncountable ordinal, which is defined as `ω_ 1` where `ω_` is the standard omega function enumerating infinite ordinals.

Ordinal.omega_eq_preOmega theorem

(o : Ordinal) : ω_ o = preOmega (ω + o)

Full source

theorem omega_eq_preOmega (o : Ordinal) : ω_ o = preOmega (ω + o) :=
  rfl

Relation between omega and pre-omega functions: $\omega_o = \text{preOmega}(\omega + o)$

Informal description

For any ordinal $o$, the omega function evaluated at $o$ equals the pre-omega function evaluated at $\omega + o$, i.e., $\omega_o = \text{preOmega}(\omega + o)$.

Ordinal.omega_strictMono theorem

: StrictMono omega

Full source

theorem omega_strictMono : StrictMono omega :=
  omega.strictMono

Strict Monotonicity of the $\omega_(-)$ Function

Informal description

The function $\omega_(-) \colon \mathrm{Ordinal} \hookrightarrow \mathrm{Ordinal}$, which enumerates the infinite initial ordinals, is strictly monotone. That is, for any ordinals $o_1$ and $o_2$, if $o_1 < o_2$ then $\omega_{o_1} < \omega_{o_2}$.

Ordinal.omega_lt_omega theorem

{o₁ o₂ : Ordinal} : ω_ o₁ < ω_ o₂ ↔ o₁ < o₂

Full source

theorem omega_lt_omega {o₁ o₂ : Ordinal} : ω_ω_ o₁ < ω_ o₂ ↔ o₁ < o₂ :=
  omega.lt_iff_lt

Strict Monotonicity of the Omega Function: $\omega_{o_1} < \omega_{o_2} \leftrightarrow o_1 < o_2$

Informal description

For any two ordinals $o_1$ and $o_2$, the infinite initial ordinal $\omega_{o_1}$ is strictly less than $\omega_{o_2}$ if and only if $o_1$ is strictly less than $o_2$.

Ordinal.omega_le_omega theorem

{o₁ o₂ : Ordinal} : ω_ o₁ ≤ ω_ o₂ ↔ o₁ ≤ o₂

Full source

theorem omega_le_omega {o₁ o₂ : Ordinal} : ω_ω_ o₁ ≤ ω_ o₂ ↔ o₁ ≤ o₂ :=
  omega.le_iff_le

Order Preservation of Omega Function: $\omega_{o_1} \leq \omega_{o_2} \leftrightarrow o_1 \leq o_2$

Informal description

For any two ordinals $o_1$ and $o_2$, the inequality $\omega_{o_1} \leq \omega_{o_2}$ holds if and only if $o_1 \leq o_2$.

Ordinal.omega_max theorem

(o₁ o₂ : Ordinal) : ω_ (max o₁ o₂) = max (ω_ o₁) (ω_ o₂)

Full source

theorem omega_max (o₁ o₂ : Ordinal) : ω_ (max o₁ o₂) = max (ω_ o₁) (ω_ o₂) :=
  omega.monotone.map_max

$\omega$ Function Preserves Maximum of Ordinals

Informal description

For any two ordinals $o₁$ and $o₂$, the $\omega$ function satisfies $\omega_{\max(o₁, o₂)} = \max(\omega_{o₁}, \omega_{o₂})$.

Ordinal.preOmega_le_omega theorem

(o : Ordinal) : preOmega o ≤ ω_ o

Full source

theorem preOmega_le_omega (o : Ordinal) : preOmega o ≤ ω_ o :=
  preOmega_le_preOmega.2 (Ordinal.le_add_left _ _)

Inequality between Pre-Omega and Omega Ordinals: $\text{preOmega}(o) \leq \omega_o$

Informal description

For any ordinal $o$, the initial ordinal $\text{preOmega}(o)$ is less than or equal to the infinite initial ordinal $\omega_o$.

Ordinal.isInitial_omega theorem

(o : Ordinal) : IsInitial (omega o)

Full source

theorem isInitial_omega (o : Ordinal) : IsInitial (omega o) :=
  isInitial_preOmega _

Initiality of $\omega_o$ for any ordinal $o$

Informal description

For any ordinal $o$, the ordinal $\omega_o$ (the $o$-th infinite initial ordinal) is initial, meaning it is the smallest ordinal with its cardinality.

Ordinal.le_omega_self theorem

(o : Ordinal) : o ≤ omega o

Full source

theorem le_omega_self (o : Ordinal) : o ≤ omega o :=
  omega_strictMono.le_apply

Ordinal Dominance by Omega: $o \leq \omega_o$

Informal description

For any ordinal $o$, the ordinal $o$ is less than or equal to the infinite initial ordinal $\omega_o$ (i.e., $o \leq \omega_o$).

Ordinal.omega_zero theorem

: ω_ 0 = ω

Full source

@[simp]
theorem omega_zero : ω_ 0 = ω := by
  rw [omega_eq_preOmega, add_zero, preOmega_omega0]

First Infinite Initial Ordinal: $\omega_0 = \omega$

Informal description

The first infinite initial ordinal $\omega_0$ is equal to the ordinal $\omega$, i.e., $\omega_0 = \omega$.

Ordinal.omega0_le_omega theorem

(o : Ordinal) : ω ≤ ω_ o

Full source

theorem omega0_le_omega (o : Ordinal) : ω ≤ ω_ o := by
  rw [← omega_zero, omega_le_omega]
  exact Ordinal.zero_le o

First Infinite Ordinal is Bounded by Omega: $\omega \leq \omega_o$

Informal description

For any ordinal $o$, the first infinite ordinal $\omega$ is less than or equal to the infinite initial ordinal $\omega_o$, i.e., $\omega \leq \omega_o$.

Ordinal.omega_pos theorem

(o : Ordinal) : 0 < ω_ o

Full source

/-- For the theorem `0 < ω`, see `omega0_pos`. -/
theorem omega_pos (o : Ordinal) : 0 < ω_ o :=
  omega0_pos.trans_le (omega0_le_omega o)

Positivity of Infinite Initial Ordinals: $0 < \omega_o$

Informal description

For any ordinal $o$, the infinite initial ordinal $\omega_o$ is strictly greater than zero, i.e., $0 < \omega_o$.

Ordinal.omega0_lt_omega1 theorem

: ω < ω₁

Full source

theorem omega0_lt_omega1 : ω < ω₁ := by
  rw [← omega_zero, omega_lt_omega]
  exact zero_lt_one

$\omega < \omega_1$

Informal description

The first infinite ordinal $\omega$ is strictly less than the first uncountable ordinal $\omega_1$.

Ordinal.isNormal_omega theorem

: IsNormal omega

Full source

theorem isNormal_omega : IsNormal omega :=
  isNormal_preOmega.trans (isNormal_add_right _)

Normality of the Omega Function

Informal description

The omega function $\omega \colon \text{Ordinal} \to \text{Ordinal}$, which enumerates the infinite initial ordinals, is a normal function. That is: 1. It is strictly increasing: for any ordinals $o_1$ and $o_2$, if $o_1 < o_2$ then $\omega(o_1) < \omega(o_2)$. 2. It is continuous at limit ordinals: for any limit ordinal $o$ and any increasing sequence $(o_i)_{i < o}$ with supremum $o$, we have $\omega(o) = \sup_{i < o} \omega(o_i)$.

Ordinal.range_omega theorem

: range omega = {x | ω ≤ x ∧ IsInitial x}

Full source

@[simp]
theorem range_omega : range omega = {x | ω ≤ x ∧ IsInitial x} := by
  ext x
  constructor
  · rintro ⟨a, rfl⟩
    exact ⟨omega0_le_omega a, isInitial_omega a⟩
  · rintro ⟨ha', ha⟩
    obtain ⟨a, rfl⟩ := ha.mem_range_preOmega
    use a - ω
    rw [omega0_le_preOmega_iff] at ha'
    rw [omega_eq_preOmega, Ordinal.add_sub_cancel_of_le ha']

Range of Omega Function: Infinite Initial Ordinals

Informal description

The range of the omega function $\omega \colon \text{Ordinal} \to \text{Ordinal}$ is the set of all ordinals $x$ such that $x$ is infinite (i.e., $\omega \leq x$) and $x$ is initial (i.e., $x$ is the smallest ordinal with its cardinality). In other words, $\text{range}(\omega) = \{x \mid \omega \leq x \text{ and } \text{IsInitial}(x)\}$.

Ordinal.mem_range_omega_iff theorem

{x : Ordinal} : x ∈ range omega ↔ ω ≤ x ∧ IsInitial x

Full source

theorem mem_range_omega_iff {x : Ordinal} : x ∈ range omegax ∈ range omega ↔ ω ≤ x ∧ IsInitial x := by
  rw [range_omega, mem_setOf]

Characterization of Ordinals in the Range of $\omega$: Infinite and Initial

Informal description

For any ordinal $x$, $x$ belongs to the range of the omega function $\omega$ if and only if $x$ is infinite (i.e., $\omega \leq x$) and initial (i.e., $x$ is the smallest ordinal with its cardinality).

Cardinal.preAleph definition

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

Full source

/-- 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`. -/
def preAleph : OrdinalOrdinal.{u}Ordinal.{u} ≃o Cardinal.{u} :=
  (enumOrdOrderIso _ not_bddAbove_isInitial).trans isInitialIso

Order isomorphism between ordinals and cardinals (pre-aleph function)

Informal description

The function $\text{preAleph}$ is an order isomorphism between the ordinals and the cardinals. It maps each ordinal $o$ to the cardinal $\text{preAleph}(o)$, where: - For finite ordinals $n$, $\text{preAleph}(n) = n$. - For $\omega$, $\text{preAleph}(\omega) = \aleph_0$. - For $\omega + 1$, $\text{preAleph}(\omega + 1) = \aleph_1$, and so on. This function serves as a preliminary version of the standard aleph function, which skips finite cardinals.

Ordinal.card_preOmega theorem

(o : Ordinal) : (preOmega o).card = preAleph o

Full source

@[simp]
theorem _root_.Ordinal.card_preOmega (o : Ordinal) : (preOmega o).card = preAleph o :=
  rfl

Cardinality of Initial Ordinal Equals Pre-Aleph Cardinal

Informal description

For any ordinal $o$, the cardinality of the initial ordinal $\text{preOmega}(o)$ is equal to the cardinal $\text{preAleph}(o)$. That is, $|\text{preOmega}(o)| = \text{preAleph}(o)$.

Cardinal.ord_preAleph theorem

(o : Ordinal) : (preAleph o).ord = preOmega o

Full source

@[simp]
theorem ord_preAleph (o : Ordinal) : (preAleph o).ord = preOmega o := by
  rw [← o.card_preOmega, (isInitial_preOmega o).ord_card]

Ordinal-Cardinal Correspondence: $\mathrm{ord}(\mathrm{preAleph}(o)) = \mathrm{preOmega}(o)$

Informal description

For any ordinal $o$, the smallest ordinal with the same cardinality as $\mathrm{preAleph}(o)$ is equal to $\mathrm{preOmega}(o)$. In other words, $\mathrm{ord}(\mathrm{preAleph}(o)) = \mathrm{preOmega}(o)$.

Cardinal.type_cardinal theorem

: typeLT Cardinal = Ordinal.univ.{u, u + 1}

Full source

@[simp]
theorem type_cardinal : typeLT Cardinal = Ordinal.univOrdinal.univ.{u, u + 1} := by
  rw [Ordinal.univ_id]
  exact Quotient.sound ⟨preAleph.symm.toRelIsoLT⟩

Order Type of Cardinal Numbers Equals Universal Ordinal

Informal description

The order type of the strict less-than relation on cardinal numbers (in universe `Type u`) is equal to the universal ordinal `Ordinal.univ.{u, u+1}`.

Cardinal.mk_cardinal theorem

: #Cardinal = univ.{u, u + 1}

Full source

@[simp]
theorem mk_cardinal : #Cardinal = univuniv.{u, u + 1} := by
  simpa only [card_type, card_univ] using congr_arg card type_cardinal

Cardinality of Cardinal Numbers Equals Universal Ordinal

Informal description

The cardinality of the type of all cardinals (in universe `Type u`) is equal to the universal ordinal `univ.{u, u+1}`.

Cardinal.preAleph_lt_preAleph theorem

{o₁ o₂ : Ordinal} : preAleph o₁ < preAleph o₂ ↔ o₁ < o₂

Full source

theorem preAleph_lt_preAleph {o₁ o₂ : Ordinal} : preAlephpreAleph o₁ < preAleph o₂ ↔ o₁ < o₂ :=
  preAleph.lt_iff_lt

Pre-aleph preserves strict order: $\text{preAleph}(o₁) < \text{preAleph}(o₂) \leftrightarrow o₁ < o₂$

Informal description

For any two ordinals $o₁$ and $o₂$, the pre-aleph cardinal $\text{preAleph}(o₁)$ is strictly less than $\text{preAleph}(o₂)$ if and only if $o₁$ is strictly less than $o₂$.

Cardinal.preAleph_le_preAleph theorem

{o₁ o₂ : Ordinal} : preAleph o₁ ≤ preAleph o₂ ↔ o₁ ≤ o₂

Full source

theorem preAleph_le_preAleph {o₁ o₂ : Ordinal} : preAlephpreAleph o₁ ≤ preAleph o₂ ↔ o₁ ≤ o₂ :=
  preAleph.le_iff_le

Pre-aleph Order Preservation: $\text{preAleph}(o_1) \leq \text{preAleph}(o_2) \leftrightarrow o_1 \leq o_2$

Informal description

For any two ordinals $o_1$ and $o_2$, the pre-aleph cardinal $\text{preAleph}(o_1)$ is less than or equal to $\text{preAleph}(o_2)$ if and only if $o_1 \leq o_2$.

Cardinal.preAleph_max theorem

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

Full source

theorem preAleph_max (o₁ o₂ : Ordinal) : preAleph (max o₁ o₂) = max (preAleph o₁) (preAleph o₂) :=
  preAleph.monotone.map_max

Pre-aleph Preserves Maximum: $\text{preAleph}(\max(o_1, o_2)) = \max(\text{preAleph}(o_1), \text{preAleph}(o_2))$

Informal description

For any two ordinals $o_1$ and $o_2$, the pre-aleph function satisfies $\text{preAleph}(\max(o_1, o_2)) = \max(\text{preAleph}(o_1), \text{preAleph}(o_2))$.

Cardinal.preAleph_zero theorem

: preAleph 0 = 0

Full source

@[simp]
theorem preAleph_zero : preAleph 0 = 0 :=
  preAleph.map_bot

Pre-aleph at Zero: $\text{preAleph}(0) = 0$

Informal description

The pre-aleph function evaluated at the ordinal zero returns the cardinal zero, i.e., $\text{preAleph}(0) = 0$.

Cardinal.preAleph_succ theorem

(o : Ordinal) : preAleph (succ o) = succ (preAleph o)

Full source

@[simp]
theorem preAleph_succ (o : Ordinal) : preAleph (succ o) = succ (preAleph o) :=
  preAleph.map_succ o

Successor Preservation of the Pre-Aleph Function: $\text{preAleph}(\text{succ}(o)) = \text{succ}(\text{preAleph}(o))$

Informal description

For any ordinal $o$, the pre-aleph function satisfies $\text{preAleph}(\text{succ}(o)) = \text{succ}(\text{preAleph}(o))$, where $\text{succ}$ denotes the successor operation on ordinals and cardinals respectively.

Cardinal.preAleph_nat theorem

(n : ℕ) : preAleph n = n

Full source

@[simp]
theorem preAleph_nat (n : ℕ) : preAleph n = n := by
  rw [← card_preOmega, preOmega_natCast, card_nat]

Pre-aleph Function on Natural Numbers: $\text{preAleph}(n) = n$

Informal description

For any natural number $n$, the pre-aleph function evaluated at $n$ equals $n$, i.e., $\text{preAleph}(n) = n$.

Cardinal.preAleph_omega0 theorem

: preAleph ω = ℵ₀

Full source

@[simp]
theorem preAleph_omega0 : preAleph ω = ℵ₀ := by
  rw [← card_preOmega, preOmega_omega0, card_omega0]

Pre-aleph at $\omega$: $\text{preAleph}(\omega) = \aleph_0$

Informal description

The pre-aleph function evaluated at the ordinal $\omega$ equals the cardinal $\aleph_0$, i.e., $\text{preAleph}(\omega) = \aleph_0$.

Cardinal.preAleph_pos theorem

{o : Ordinal} : 0 < preAleph o ↔ 0 < o

Full source

@[simp]
theorem preAleph_pos {o : Ordinal} : 0 < preAleph o ↔ 0 < o := by
  rw [← preAleph_zero, preAleph_lt_preAleph]

Positivity of Pre-Aleph: $\text{preAleph}(o) > 0 \leftrightarrow o > 0$

Informal description

For any ordinal $o$, the pre-aleph cardinal $\text{preAleph}(o)$ is strictly greater than zero if and only if the ordinal $o$ is strictly greater than zero. In other words, $0 < \text{preAleph}(o) \leftrightarrow 0 < o$.

Cardinal.aleph0_le_preAleph theorem

{o : Ordinal} : ℵ₀ ≤ preAleph o ↔ ω ≤ o

Full source

@[simp]
theorem aleph0_le_preAleph {o : Ordinal} : ℵ₀ℵ₀ ≤ preAleph o ↔ ω ≤ o := by
  rw [← preAleph_omega0, preAleph_le_preAleph]

$\aleph_0 \leq \text{preAleph}(o) \leftrightarrow \omega \leq o$

Informal description

For any ordinal $o$, the cardinal $\aleph_0$ is less than or equal to $\text{preAleph}(o)$ if and only if the ordinal $\omega$ is less than or equal to $o$.

Cardinal.lift_preAleph theorem

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

Full source

@[simp]
theorem lift_preAleph (o : OrdinalOrdinal.{u}) : lift.{v} (preAleph o) = preAleph (Ordinal.lift.{v} o) :=
  (preAleph.toInitialSeg.trans liftInitialSeg).eq
    (Ordinal.liftInitialSeg.trans preAleph.toInitialSeg) o

Lift Commutes with Pre-Aleph: $\text{lift}(\text{preAleph}(o)) = \text{preAleph}(\text{lift}(o))$

Informal description

For any ordinal $o$ in universe `Type u`, the lift of the pre-aleph cardinal $\text{preAleph}(o)$ to universe `Type (max u v)` is equal to the pre-aleph cardinal of the lift of $o$ to `Type (max u v)$. That is, \[ \text{lift}(\text{preAleph}(o)) = \text{preAleph}(\text{lift}(o)). \]

Ordinal.lift_preOmega theorem

(o : Ordinal.{u}) : Ordinal.lift.{v} (preOmega o) = preOmega (Ordinal.lift.{v} o)

Full source

@[simp]
theorem _root_.Ordinal.lift_preOmega (o : OrdinalOrdinal.{u}) :
    Ordinal.lift.{v} (preOmega o) = preOmega (Ordinal.lift.{v} o) := by
  rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]

Lift Commutes with Pre-Omega: $\mathrm{lift}(\mathrm{preOmega}(o)) = \mathrm{preOmega}(\mathrm{lift}(o))$

Informal description

For any ordinal $o$ in universe `Type u`, the lift of the pre-omega ordinal $\mathrm{preOmega}(o)$ to universe `Type (max u v)$ is equal to the pre-omega ordinal of the lift of $o$ to `Type (max u v)$. That is, \[ \mathrm{lift}(\mathrm{preOmega}(o)) = \mathrm{preOmega}(\mathrm{lift}(o)). \]

Cardinal.preAleph_le_of_isLimit theorem

{o : Ordinal} (l : o.IsLimit) {c} : preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c

Full source

theorem preAleph_le_of_isLimit {o : Ordinal} (l : o.IsLimit) {c} :
    preAlephpreAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c :=
  ⟨fun h o' h' => (preAleph_le_preAleph.2 <| h'.le).trans h, fun h => by
    rw [← preAleph.apply_symm_apply c, preAleph_le_preAleph, limit_le l]
    intro x h'
    rw [← preAleph_le_preAleph, preAleph.apply_symm_apply]
    exact h _ h'⟩

Pre-aleph Cardinal at Limit Ordinal is Bounded by All Smaller Pre-aleph Cardinals

Informal description

For any limit ordinal $o$ and any cardinal $c$, the pre-aleph cardinal $\text{preAleph}(o)$ is less than or equal to $c$ if and only if for every ordinal $o' < o$, the pre-aleph cardinal $\text{preAleph}(o')$ is less than or equal to $c$.

Cardinal.preAleph_limit theorem

{o : Ordinal} (ho : o.IsLimit) : preAleph o = ⨆ a : Iio o, preAleph a

Full source

theorem preAleph_limit {o : Ordinal} (ho : o.IsLimit) : preAleph o = ⨆ a : Iio o, preAleph a := by
  refine le_antisymm ?_ (ciSup_le' fun i => preAleph_le_preAleph.2 i.2.le)
  rw [preAleph_le_of_isLimit ho]
  exact fun a ha => le_ciSup (bddAbove_of_small _) (⟨a, ha⟩ : Iio o)

Pre-aleph Cardinal at Limit Ordinal is Supremum of Smaller Pre-aleph Cardinals

Informal description

For any limit ordinal $o$, the pre-aleph cardinal $\text{preAleph}(o)$ is equal to the supremum of all pre-aleph cardinals $\text{preAleph}(a)$ where $a$ ranges over all ordinals less than $o$. In other words: $$\text{preAleph}(o) = \bigsqcup_{a < o} \text{preAleph}(a)$$

Cardinal.preAleph_le_of_strictMono theorem

{f : Ordinal → Cardinal} (hf : StrictMono f) (o : Ordinal) : preAleph o ≤ f o

Full source

theorem preAleph_le_of_strictMono {f : Ordinal → Cardinal} (hf : StrictMono f) (o : Ordinal) :
    preAleph o ≤ f o := by
  simpa using (hf.comp preAleph.symm.strictMono).id_le (preAleph o)

Pre-aleph function is dominated by strictly monotone functions

Informal description

For any strictly monotone function $f$ from ordinals to cardinals and for any ordinal $o$, the pre-aleph function evaluated at $o$ is less than or equal to $f(o)$, i.e., $\text{preAleph}(o) \leq f(o)$.

Cardinal.aleph definition

: Ordinal ↪o Cardinal

Full source

/-- 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`. -/
def aleph : OrdinalOrdinal ↪o Cardinal :=
  (OrderEmbedding.addLeft ω).trans preAleph.toOrderEmbedding

Aleph function (infinite cardinals enumeration)

Informal description

The function $\aleph$ maps an ordinal number $o$ to the infinite cardinal number $\aleph_o$, where $\aleph_0$ is the first infinite cardinal (the cardinality of $\mathbb{N}$), $\aleph_1$ is the next larger cardinal, and so on. This function is defined as the composition of the order embedding that shifts ordinals by $\omega$ (to skip finite cardinals) followed by the pre-aleph function.

Cardinal.termℵ_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped notation "ℵ_ " => aleph

Aleph function notation

Informal description

The notation `ℵ_` is used to represent the aleph function, which maps an ordinal number to its corresponding infinite cardinal number. Specifically, `ℵ_ o` denotes the `o`-th infinite cardinal number (where `o` is an ordinal).

Cardinal.termℵ₁ definition

: Lean.ParserDescr✝

Full source

/-- `ℵ₁` is the first uncountable cardinal. -/
scoped notation "ℵ₁" => ℵ_ 1

First uncountable cardinal ($\aleph_1$)

Informal description

The notation $\aleph_1$ represents the first uncountable cardinal.

Cardinal.aleph_eq_preAleph theorem

(o : Ordinal) : ℵ_ o = preAleph (ω + o)

Full source

theorem aleph_eq_preAleph (o : Ordinal) : ℵ_ o = preAleph (ω + o) :=
  rfl

Aleph Function as Shifted Pre-Aleph: $\aleph_o = \text{preAleph}(\omega + o)$

Informal description

For any ordinal number $o$, the $\aleph$ function satisfies $\aleph_o = \text{preAleph}(\omega + o)$, where $\omega$ is the first infinite ordinal and $\text{preAleph}$ is the order isomorphism between ordinals and cardinals.

Ordinal.card_omega theorem

(o : Ordinal) : (ω_ o).card = ℵ_ o

Full source

@[simp]
theorem _root_.Ordinal.card_omega (o : Ordinal) : (ω_ o).card = ℵ_ o :=
  rfl

Cardinality of Initial Ordinal $\omega_o$ is $\aleph_o$

Informal description

For any ordinal $o$, the cardinality of the initial ordinal $\omega_o$ is equal to the aleph cardinal $\aleph_o$. That is, $|\omega_o| = \aleph_o$.

Cardinal.ord_aleph theorem

(o : Ordinal) : (ℵ_ o).ord = ω_ o

Full source

@[simp]
theorem ord_aleph (o : Ordinal) : (ℵ_ o).ord = ω_ o :=
  ord_preAleph _

Ordinal-Cardinal Correspondence: $\mathrm{ord}(\aleph_o) = \omega_o$

Informal description

For any ordinal $o$, the smallest ordinal with the same cardinality as $\aleph_o$ is equal to $\omega_o$. That is, $\mathrm{ord}(\aleph_o) = \omega_o$.

Cardinal.aleph_lt_aleph theorem

{o₁ o₂ : Ordinal} : ℵ_ o₁ < ℵ_ o₂ ↔ o₁ < o₂

Full source

theorem aleph_lt_aleph {o₁ o₂ : Ordinal} : ℵ_ℵ_ o₁ < ℵ_ o₂ ↔ o₁ < o₂ :=
  aleph.lt_iff_lt

$\aleph_{o_1} < \aleph_{o_2} \leftrightarrow o_1 < o_2$

Informal description

For any two ordinals $o_1$ and $o_2$, the cardinal $\aleph_{o_1}$ is strictly less than $\aleph_{o_2}$ if and only if $o_1$ is strictly less than $o_2$.

Cardinal.aleph_le_aleph theorem

{o₁ o₂ : Ordinal} : ℵ_ o₁ ≤ ℵ_ o₂ ↔ o₁ ≤ o₂

Full source

theorem aleph_le_aleph {o₁ o₂ : Ordinal} : ℵ_ℵ_ o₁ ≤ ℵ_ o₂ ↔ o₁ ≤ o₂ :=
  aleph.le_iff_le

Monotonicity of Aleph Function: $\aleph_{o₁} \leq \aleph_{o₂} \leftrightarrow o₁ \leq o₂$

Informal description

For any two ordinals $o₁$ and $o₂$, the inequality $\aleph_{o₁} \leq \aleph_{o₂}$ holds if and only if $o₁ \leq o₂$.

Cardinal.aleph_max theorem

(o₁ o₂ : Ordinal) : ℵ_ (max o₁ o₂) = max (ℵ_ o₁) (ℵ_ o₂)

Full source

theorem aleph_max (o₁ o₂ : Ordinal) : ℵ_ (max o₁ o₂) = max (ℵ_ o₁) (ℵ_ o₂) :=
  aleph.monotone.map_max

$\aleph$ Function Preserves Maximum: $\aleph_{\max(o₁, o₂)} = \max(\aleph_{o₁}, \aleph_{o₂})$

Informal description

For any two ordinals $o₁$ and $o₂$, the $\aleph$ function satisfies $\aleph_{\max(o₁, o₂)} = \max(\aleph_{o₁}, \aleph_{o₂})$.

Cardinal.preAleph_le_aleph theorem

(o : Ordinal) : preAleph o ≤ ℵ_ o

Full source

theorem preAleph_le_aleph (o : Ordinal) : preAleph o ≤ ℵ_ o :=
  preAleph_le_preAleph.2 (Ordinal.le_add_left _ _)

Pre-aleph is bounded by aleph: $\text{preAleph}(o) \leq \aleph_o$

Informal description

For any ordinal $o$, the pre-aleph cardinal $\text{preAleph}(o)$ is less than or equal to the aleph cardinal $\aleph_o$.

Cardinal.aleph_succ theorem

(o : Ordinal) : ℵ_ (succ o) = succ (ℵ_ o)

Full source

@[simp]
theorem aleph_succ (o : Ordinal) : ℵ_ (succ o) = succ (ℵ_ o) := by
  rw [aleph_eq_preAleph, add_succ, preAleph_succ, aleph_eq_preAleph]

Successor Preservation of the Aleph Function: $\aleph_{\text{succ}(o)} = \text{succ}(\aleph_o)$

Informal description

For any ordinal $o$, the aleph function satisfies $\aleph_{\text{succ}(o)} = \text{succ}(\aleph_o)$, where $\text{succ}$ denotes the successor operation on ordinals and cardinals respectively.

Cardinal.aleph_zero theorem

: ℵ_ 0 = ℵ₀

Full source

@[simp]
theorem aleph_zero : ℵ_ 0 = ℵ₀ := by rw [aleph_eq_preAleph, add_zero, preAleph_omega0]

Aleph Function at Zero: $\aleph_0 = \aleph_0$

Informal description

The aleph function evaluated at the ordinal $0$ equals the first infinite cardinal $\aleph_0$, i.e., $\aleph_0 = \aleph_0$.

Cardinal.lift_aleph theorem

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

Full source

@[simp]
theorem lift_aleph (o : OrdinalOrdinal.{u}) : lift.{v} (aleph o) = aleph (Ordinal.lift.{v} o) := by
  simp [aleph_eq_preAleph]

Lift Commutes with Aleph: $\text{lift}(\aleph_o) = \aleph_{\text{lift}(o)}$

Informal description

For any ordinal $o$ in universe `Type u`, the lift of the aleph cardinal $\aleph_o$ to universe `Type (max u v)$ is equal to the aleph cardinal of the lift of $o$ to `Type (max u v)$. That is, \[ \text{lift}(\aleph_o) = \aleph_{\text{lift}(o)}. \]

Ordinal.lift_omega theorem

(o : Ordinal.{u}) : Ordinal.lift.{v} (ω_ o) = ω_ (Ordinal.lift.{v} o)

Full source

/-- For the theorem `lift ω = ω`, see `lift_omega0`. -/
@[simp]
theorem _root_.Ordinal.lift_omega (o : OrdinalOrdinal.{u}) :
    Ordinal.lift.{v} (ω_ o) = ω_ (Ordinal.lift.{v} o) := by
  simp [omega_eq_preOmega]

Lift Commutes with Omega: $\mathrm{lift}(\omega_o) = \omega_{\mathrm{lift}(o)}$

Informal description

For any ordinal $o$ in universe `Type u`, the lift of the infinite initial ordinal $\omega_o$ to universe `Type (max u v)$ is equal to the infinite initial ordinal indexed by the lift of $o$ to `Type (max u v)$. That is, \[ \mathrm{lift}(\omega_o) = \omega_{\mathrm{lift}(o)}. \]

Cardinal.aleph_limit theorem

{o : Ordinal} (ho : o.IsLimit) : ℵ_ o = ⨆ a : Iio o, ℵ_ a

Full source

theorem aleph_limit {o : Ordinal} (ho : o.IsLimit) : ℵ_ o = ⨆ a : Iio o, ℵ_ a := by
  rw [aleph_eq_preAleph, preAleph_limit (isLimit_add ω ho)]
  apply le_antisymm <;>
    apply ciSup_mono' (bddAbove_of_small _) <;>
    intro i
  · refine ⟨⟨_, sub_lt_of_lt_add i.2 ho.pos⟩, ?_⟩
    simpa [aleph_eq_preAleph] using le_add_sub _ _
  · exact ⟨⟨_, add_lt_add_left i.2 ω⟩, le_rfl⟩

Aleph Cardinal at Limit Ordinal is Supremum of Smaller Aleph Cardinals

Informal description

For any limit ordinal $o$, the aleph cardinal $\aleph_o$ is equal to the supremum of all aleph cardinals $\aleph_a$ where $a$ ranges over all ordinals less than $o$. In other words: $$\aleph_o = \bigsqcup_{a < o} \aleph_a$$

Cardinal.aleph0_le_aleph theorem

(o : Ordinal) : ℵ₀ ≤ ℵ_ o

Full source

theorem aleph0_le_aleph (o : Ordinal) : ℵ₀ ≤ ℵ_ o := by
  rw [aleph_eq_preAleph, aleph0_le_preAleph]
  apply Ordinal.le_add_right

$\aleph_0 \leq \aleph_o$ for all ordinals $o$

Informal description

For every ordinal number $o$, the cardinal $\aleph_0$ is less than or equal to $\aleph_o$.

Cardinal.aleph_pos theorem

(o : Ordinal) : 0 < ℵ_ o

Full source

theorem aleph_pos (o : Ordinal) : 0 < ℵ_ o :=
  aleph0_pos.trans_le (aleph0_le_aleph o)

Positivity of Aleph Cardinals: $0 < \aleph_o$ for all ordinals $o$

Informal description

For every ordinal number $o$, the aleph cardinal $\aleph_o$ is strictly greater than zero, i.e., $0 < \aleph_o$.

Cardinal.aleph_toNat theorem

(o : Ordinal) : toNat (ℵ_ o) = 0

Full source

@[simp]
theorem aleph_toNat (o : Ordinal) : toNat (ℵ_ o) = 0 :=
  toNat_apply_of_aleph0_le <| aleph0_le_aleph o

Projection of Aleph Numbers to Zero: $\mathrm{toNat}(\aleph_o) = 0$

Informal description

For any ordinal number $o$, the projection of the aleph number $\aleph_o$ to natural numbers is zero, i.e., $\mathrm{toNat}(\aleph_o) = 0$.

Cardinal.aleph_toENat theorem

(o : Ordinal) : toENat (ℵ_ o) = ⊤

Full source

@[simp]
theorem aleph_toENat (o : Ordinal) : toENat (ℵ_ o) = ⊤ :=
  (toENat_eq_top.2 (aleph0_le_aleph o))

$\mathrm{toENat}(\aleph_o) = \infty$ for all ordinals $o$

Informal description

For any ordinal number $o$, the extended natural number projection of the aleph number $\aleph_o$ is $\infty$. In other words, $\mathrm{toENat}(\aleph_o) = \infty$.

Cardinal.isLimit_omega theorem

(o : Ordinal) : Ordinal.IsLimit (ω_ o)

Full source

theorem isLimit_omega (o : Ordinal) : Ordinal.IsLimit (ω_ o) := by
  rw [← ord_aleph]
  exact isLimit_ord (aleph0_le_aleph _)

$\omega_o$ is a limit ordinal for all $o$

Informal description

For every ordinal $o$, the ordinal $\omega_o$ is a limit ordinal (i.e., it has no immediate predecessor and is not zero).

Cardinal.range_aleph theorem

: range aleph = Set.Ici ℵ₀

Full source

@[simp]
theorem range_aleph : range aleph = Set.Ici ℵ₀ := by
  ext c
  refine ⟨fun ⟨o, e⟩ => e ▸ aleph0_le_aleph _, fun hc ↦ ⟨preAleph.symm c - ω, ?_⟩⟩
  rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]
  rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]

Range of Aleph Function Equals Infinite Cardinals

Informal description

The range of the aleph function is equal to the set of all infinite cardinals, i.e., $\text{range}(\aleph) = \{c \mid \aleph_0 \leq c\}$.

Cardinal.mem_range_aleph_iff theorem

{c : Cardinal} : c ∈ range aleph ↔ ℵ₀ ≤ c

Full source

theorem mem_range_aleph_iff {c : Cardinal} : c ∈ range alephc ∈ range aleph ↔ ℵ₀ ≤ c := by
  rw [range_aleph, mem_Ici]

Characterization of Cardinals in the Range of Aleph Function: $c \in \text{range}(\aleph) \leftrightarrow \aleph_0 \leq c$

Informal description

A cardinal $c$ belongs to the range of the aleph function if and only if $c$ is an infinite cardinal, i.e., $\aleph_0 \leq c$.

Cardinal.succ_aleph0 theorem

: succ ℵ₀ = ℵ₁

Full source

@[simp]
theorem succ_aleph0 : succ ℵ₀ = ℵ₁ := by
  rw [← aleph_zero, ← aleph_succ, Ordinal.succ_zero]

Successor of $\aleph_0$ is $\aleph_1$

Informal description

The successor of the first infinite cardinal $\aleph_0$ is equal to the next cardinal $\aleph_1$, i.e., $\text{succ}(\aleph_0) = \aleph_1$.

Cardinal.aleph0_lt_aleph_one theorem

: ℵ₀ < ℵ₁

Full source

theorem aleph0_lt_aleph_one : ℵ₀ < ℵ₁ := by
  rw [← succ_aleph0]
  apply lt_succ

$\aleph_0 < \aleph_1$ (Strict inequality between first two infinite cardinals)

Informal description

The first infinite cardinal $\aleph_0$ is strictly less than the next cardinal $\aleph_1$, i.e., $\aleph_0 < \aleph_1$.

Cardinal.countable_iff_lt_aleph_one theorem

{α : Type*} (s : Set α) : s.Countable ↔ #s < ℵ₁

Full source

theorem countable_iff_lt_aleph_one {α : Type*} (s : Set α) : s.Countable ↔ #s < ℵ₁ := by
  rw [← succ_aleph0, lt_succ_iff, le_aleph0_iff_set_countable]

Countability Criterion: $s$ countable $\leftrightarrow \#s < \aleph_1$

Informal description

For any set $s$ of elements of type $\alpha$, $s$ is countable if and only if its cardinality is strictly less than $\aleph_1$.

Cardinal.aleph1_le_lift theorem

{c : Cardinal.{u}} : ℵ₁ ≤ lift.{v} c ↔ ℵ₁ ≤ c

Full source

@[simp]
theorem aleph1_le_lift {c : CardinalCardinal.{u}} : ℵ₁ℵ₁ ≤ lift.{v} c ↔ ℵ₁ ≤ c := by
  simpa using lift_le (a := ℵ₁)

Lift Preserves Aleph-One Inequality: $\aleph_1 \leq \text{lift}(c) \leftrightarrow \aleph_1 \leq c$

Informal description

For any cardinal number $c$ in universe `Type u`, the inequality $\aleph_1 \leq \text{lift}_{v}(c)$ holds if and only if $\aleph_1 \leq c$ holds in the original universe.

Cardinal.lift_le_aleph1 theorem

{c : Cardinal.{u}} : lift.{v} c ≤ ℵ₁ ↔ c ≤ ℵ₁

Full source

@[simp]
theorem lift_le_aleph1 {c : CardinalCardinal.{u}} : liftlift.{v} c ≤ ℵ₁ ↔ c ≤ ℵ₁ := by
  simpa using lift_le (b := ℵ₁)

Lift Preserves Inequality with $\aleph_1$: $\text{lift}(c) \leq \aleph_1 \leftrightarrow c \leq \aleph_1$

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)$ is less than or equal to $\aleph_1$ if and only if $c \leq \aleph_1$ in the original universe.

Cardinal.aleph1_lt_lift theorem

{c : Cardinal.{u}} : ℵ₁ < lift.{v} c ↔ ℵ₁ < c

Full source

@[simp]
theorem aleph1_lt_lift {c : CardinalCardinal.{u}} : ℵ₁ℵ₁ < lift.{v} c ↔ ℵ₁ < c := by
  simpa using lift_lt (a := ℵ₁)

Preservation of $\aleph_1$ Strict Order under Cardinal Lift: $\aleph_1 < \text{lift}(c) \leftrightarrow \aleph_1 < c$

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)$ satisfies $\aleph_1 < \text{lift}(c)$ if and only if $\aleph_1 < c$ in the original universe.

Cardinal.lift_lt_aleph1 theorem

{c : Cardinal.{u}} : lift.{v} c < ℵ₁ ↔ c < ℵ₁

Full source

@[simp]
theorem lift_lt_aleph1 {c : CardinalCardinal.{u}} : liftlift.{v} c < ℵ₁ ↔ c < ℵ₁ := by
  simpa using lift_lt (b := ℵ₁)

Preservation of Strict Order under Cardinal Lift: $\text{lift}(c) < \aleph_1 \leftrightarrow c < \aleph_1$

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)` is strictly less than $\aleph_1$ if and only if $c$ is strictly less than $\aleph_1$ in the original universe. That is, \[ \text{lift}_{v,u}(c) < \aleph_1 \leftrightarrow c < \aleph_1. \]

Cardinal.aleph1_eq_lift theorem

{c : Cardinal.{u}} : ℵ₁ = lift.{v} c ↔ ℵ₁ = c

Full source

@[simp]
theorem aleph1_eq_lift {c : CardinalCardinal.{u}} : ℵ₁ℵ₁ = lift.{v} c ↔ ℵ₁ = c := by
  simpa using lift_inj (a := ℵ₁)

Lift Invariance of $\aleph_1$: $\aleph_1 = \text{lift}(c) \leftrightarrow \aleph_1 = c$

Informal description

For any cardinal number $c$ in universe `Type u`, the first uncountable cardinal $\aleph_1$ is equal to the lift of $c$ to universe `Type (max u v)` if and only if $\aleph_1$ is equal to $c$ in the original universe. That is, \[ \aleph_1 = \text{lift}(c) \leftrightarrow \aleph_1 = c. \]

Cardinal.lift_eq_aleph1 theorem

{c : Cardinal.{u}} : lift.{v} c = ℵ₁ ↔ c = ℵ₁

Full source

@[simp]
theorem lift_eq_aleph1 {c : CardinalCardinal.{u}} : liftlift.{v} c = ℵ₁ ↔ c = ℵ₁ := by
  simpa using lift_inj (b := ℵ₁)

Lift Equivalence for $\aleph_1$: $\text{lift}(c) = \aleph_1 \leftrightarrow c = \aleph_1$

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)` equals $\aleph_1$ if and only if $c$ equals $\aleph_1$ in the original universe. That is, \[ \text{lift}(c) = \aleph_1 \leftrightarrow c = \aleph_1. \]

Cardinal.lt_omega_iff_card_lt theorem

{x o : Ordinal} : x < ω_ o ↔ x.card < ℵ_ o

Full source

theorem lt_omega_iff_card_lt {x o : Ordinal} : x < ω_ o ↔ x.card < ℵ_ o := by
  rw [← (isInitial_omega o).card_lt_card, card_omega]

Ordinal Comparison via Cardinality: $x < \omega_o \leftrightarrow |x| < \aleph_o$

Informal description

For any ordinals $x$ and $o$, the ordinal $x$ is less than $\omega_o$ if and only if the cardinality of $x$ is less than $\aleph_o$. In symbols: $$ x < \omega_o \leftrightarrow |x| < \aleph_o $$

Cardinal.preBeth definition

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

Full source

/-- 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`. -/
def preBeth (o : OrdinalOrdinal.{u}) : CardinalCardinal.{u} :=
  ⨆ a : Iio o, 2 ^ preBeth a
termination_by o
decreasing_by exact a.2

Pre-beth function (starting at 0)

Informal description

The "pre-beth" function $\text{preBeth}(o)$ is defined for an ordinal $o$ as the supremum of $2^{\text{preBeth}(a)}$ for all $a < o$. This ensures that: - $\text{preBeth}(0) = 0$, - $\text{preBeth}(o+1) = 2^{\text{preBeth}(o)}$ for successor ordinals, and - For a limit ordinal $o$, $\text{preBeth}(o)$ is the supremum of $\text{preBeth}(a)$ for all $a < o$.

Cardinal.preBeth_strictMono theorem

: StrictMono preBeth

Full source

theorem preBeth_strictMono : StrictMono preBeth := by
  intro a b h
  conv_rhs => rw [preBeth]
  rw [lt_ciSup_iff' (bddAbove_of_small _)]
  exact ⟨⟨a, h⟩, cantor _⟩

Strict Monotonicity of the Pre-Beth Function

Informal description

The pre-beth function $\text{preBeth} : \text{Ordinal} \to \text{Cardinal}$ is strictly increasing. That is, for any ordinals $o_1$ and $o_2$, if $o_1 < o_2$, then $\text{preBeth}(o_1) < \text{preBeth}(o_2)$.

Cardinal.preBeth_mono theorem

: Monotone preBeth

Full source

theorem preBeth_mono : Monotone preBeth :=
  preBeth_strictMono.monotone

Monotonicity of the Pre-Beth Function

Informal description

The pre-beth function $\text{preBeth} : \text{Ordinal} \to \text{Cardinal}$ is monotone. That is, for any ordinals $o_1$ and $o_2$, if $o_1 \leq o_2$, then $\text{preBeth}(o_1) \leq \text{preBeth}(o_2)$.

Cardinal.preAleph_le_preBeth theorem

(o : Ordinal) : preAleph o ≤ preBeth o

Full source

theorem preAleph_le_preBeth (o : Ordinal) : preAleph o ≤ preBeth o :=
  preAleph_le_of_strictMono preBeth_strictMono o

Pre-aleph is dominated by pre-beth: $\text{preAleph}(o) \leq \text{preBeth}(o)$ for all ordinals $o$

Informal description

For any ordinal $o$, the pre-aleph cardinal $\text{preAleph}(o)$ is less than or equal to the pre-beth cardinal $\text{preBeth}(o)$. That is, $\text{preAleph}(o) \leq \text{preBeth}(o)$.

Cardinal.preBeth_lt_preBeth theorem

{o₁ o₂ : Ordinal} : preBeth o₁ < preBeth o₂ ↔ o₁ < o₂

Full source

@[simp]
theorem preBeth_lt_preBeth {o₁ o₂ : Ordinal} : preBethpreBeth o₁ < preBeth o₂ ↔ o₁ < o₂ :=
  preBeth_strictMono.lt_iff_lt

Strict Monotonicity of Pre-Beth Function: $\text{preBeth}(o₁) < \text{preBeth}(o₂) \leftrightarrow o₁ < o₂$

Informal description

For any two ordinals $o₁$ and $o₂$, the pre-beth cardinal $\text{preBeth}(o₁)$ is strictly less than $\text{preBeth}(o₂)$ if and only if $o₁$ is strictly less than $o₂$.

Cardinal.preBeth_le_preBeth theorem

{o₁ o₂ : Ordinal} : preBeth o₁ ≤ preBeth o₂ ↔ o₁ ≤ o₂

Full source

@[simp]
theorem preBeth_le_preBeth {o₁ o₂ : Ordinal} : preBethpreBeth o₁ ≤ preBeth o₂ ↔ o₁ ≤ o₂ :=
  preBeth_strictMono.le_iff_le

Pre-beth Function Monotonicity: $\text{preBeth}(o_1) \leq \text{preBeth}(o_2) \leftrightarrow o_1 \leq o_2$

Informal description

For any two ordinals $o_1$ and $o_2$, the inequality $\text{preBeth}(o_1) \leq \text{preBeth}(o_2)$ holds if and only if $o_1 \leq o_2$.

Cardinal.preBeth_zero theorem

: preBeth 0 = 0

Full source

@[simp]
theorem preBeth_zero : preBeth 0 = 0 := by
  rw [preBeth]
  simp

Pre-beth Function at Zero: $\text{preBeth}(0) = 0$

Informal description

The pre-beth function evaluated at the ordinal $0$ is equal to the cardinal $0$, i.e., $\text{preBeth}(0) = 0$.

Cardinal.preBeth_succ theorem

(o : Ordinal) : preBeth (succ o) = 2 ^ preBeth o

Full source

@[simp]
theorem preBeth_succ (o : Ordinal) : preBeth (succ o) = 2 ^ preBeth o := by
  rw [preBeth, Iio_succ]
  apply (le_ciSup (bddAbove_of_small _) (⟨o, le_refl o⟩ : Iic o)).antisymm'
  rw [ciSup_le_iff' (bddAbove_of_small _)]
  rintro ⟨a, h⟩
  exact power_le_power_left two_ne_zero (preBeth_mono h)

Successor Property of the Pre-Beth Function: $\operatorname{preBeth}(\operatorname{succ}(o)) = 2^{\operatorname{preBeth}(o)}$

Informal description

For any ordinal $o$, the pre-beth function evaluated at the successor ordinal $\operatorname{succ}(o)$ is equal to $2$ raised to the power of $\operatorname{preBeth}(o)$, i.e., \[ \operatorname{preBeth}(\operatorname{succ}(o)) = 2^{\operatorname{preBeth}(o)}. \]

Cardinal.preBeth_limit theorem

{o : Ordinal} (ho : IsSuccPrelimit o) : preBeth o = ⨆ a : Iio o, preBeth a

Full source

theorem preBeth_limit {o : Ordinal} (ho : IsSuccPrelimit o) :
    preBeth o = ⨆ a : Iio o, preBeth a := by
  rw [preBeth]
  apply (ciSup_mono (bddAbove_of_small _) fun _ ↦ (cantor _).le).antisymm'
  rw [ciSup_le_iff' (bddAbove_of_small _)]
  intro a
  rw [← preBeth_succ]
  exact le_ciSup (bddAbove_of_small _) (⟨_, ho.succ_lt a.2⟩ : Iio o)

Limit Property of the Pre-Beth Function: $\text{preBeth}(o) = \sup_{a < o} \text{preBeth}(a)$ for successor pre-limit ordinals $o$

Informal description

For any ordinal $o$ that is a successor pre-limit (i.e., there is no element covered by $o$ in the order), the pre-beth function evaluated at $o$ is equal to the supremum of the pre-beth function evaluated at all ordinals less than $o$. In symbols: \[ \text{preBeth}(o) = \bigsqcup_{a < o} \text{preBeth}(a). \]

Cardinal.preBeth_nat theorem

: ∀ n : ℕ, preBeth n = (2 ^ ·)^[n] (0 : ℕ)

Full source

theorem preBeth_nat : ∀ n : ℕ, preBeth n = (2 ^ ·)^[n] (0 : ℕ)
 | 0 => by simp
 | (n + 1) => by
    rw [natCast_succ, preBeth_succ, Function.iterate_succ_apply', preBeth_nat]
    simp

Pre-Beth Function on Natural Numbers as Iterated Exponentiation: $\operatorname{preBeth}(n) = (2^{(\cdot)})^{[n]}(0)$

Informal description

For any natural number $n$, the pre-beth function evaluated at $n$ is equal to the $n$-th iterate of the function $\lambda k, 2^k$ applied to $0$, i.e., \[ \operatorname{preBeth}(n) = (2^{(\cdot)})^{[n]}(0). \]

Cardinal.preBeth_one theorem

: preBeth 1 = 1

Full source

@[simp]
theorem preBeth_one : preBeth 1 = 1 := by
  simpa using preBeth_nat 1

Pre-Beth Function at One: $\text{preBeth}(1) = 1$

Informal description

The pre-beth function evaluated at the ordinal $1$ equals $1$, i.e., $\text{preBeth}(1) = 1$.

Cardinal.preBeth_omega theorem

: preBeth ω = ℵ₀

Full source

@[simp]
theorem preBeth_omega : preBeth ω = ℵ₀ := by
  apply le_antisymm
  · rw [preBeth_limit isLimit_omega0.isSuccPrelimit, ciSup_le_iff' (bddAbove_of_small _)]
    rintro ⟨a, ha⟩
    obtain ⟨n, rfl⟩ := lt_omega0.1 ha
    rw [preBeth_nat]
    exact (nat_lt_aleph0 _).le
  · simpa using preAleph_le_preBeth ω

Pre-Beth Function at $\omega$: $\text{preBeth}(\omega) = \aleph_0$

Informal description

The pre-beth function evaluated at the ordinal $\omega$ equals the cardinal $\aleph_0$, i.e., $\text{preBeth}(\omega) = \aleph_0$.

Cardinal.preBeth_pos theorem

{o : Ordinal} : 0 < preBeth o ↔ 0 < o

Full source

@[simp]
theorem preBeth_pos {o : Ordinal} : 0 < preBeth o ↔ 0 < o := by
  simpa using preBeth_lt_preBeth (o₁ := 0)

Positivity of Pre-Beth Function: $0 < \text{preBeth}(o) \leftrightarrow 0 < o$

Informal description

For any ordinal $o$, the pre-beth cardinal $\text{preBeth}(o)$ is strictly positive if and only if the ordinal $o$ is strictly positive.

Cardinal.isNormal_preBeth theorem

: IsNormal (ord ∘ preBeth)

Full source

theorem isNormal_preBeth : IsNormal (ordord ∘ preBeth) := by
  refine (isNormal_iff_strictMono_limit _).2
    ⟨ord_strictMono.comp preBeth_strictMono, fun o ho a ha ↦ ?_⟩
  rw [comp_apply, preBeth_limit ho.isSuccPrelimit, ord_le]
  exact ciSup_le' fun b => ord_le.1 (ha _ b.2)

Normality of the Ordinal Embedding of the Pre-Beth Function

Informal description

The composition of the ordinal embedding function $\mathrm{ord}$ with the pre-beth function $\mathrm{preBeth}$ is a normal function. That is: 1. It is strictly increasing: for any ordinals $o_1 < o_2$, we have $\mathrm{ord}(\mathrm{preBeth}(o_1)) < \mathrm{ord}(\mathrm{preBeth}(o_2))$. 2. It is continuous at limit ordinals: for any limit ordinal $o$, we have $\mathrm{ord}(\mathrm{preBeth}(o)) = \sup_{a < o} \mathrm{ord}(\mathrm{preBeth}(a))$.

Cardinal.beth definition

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

Full source

/-- 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`. -/
def beth (o : OrdinalOrdinal.{u}) : CardinalCardinal.{u} :=
  preBeth (ω + o)

Beth function (starting at $\aleph_0$)

Informal description

The Beth function $\beth(o)$ is defined for an ordinal $o$ as $\text{preBeth}(\omega + o)$, where $\text{preBeth}$ is the function that satisfies: - $\text{preBeth}(0) = 0$, - $\text{preBeth}(o+1) = 2^{\text{preBeth}(o)}$ for successor ordinals, and - For a limit ordinal $o$, $\text{preBeth}(o)$ is the supremum of $\text{preBeth}(a)$ for all $a < o$. This ensures that $\beth$ starts at $\aleph_0$ (i.e., $\beth(0) = \aleph_0$) and grows exponentially at successor ordinals while being continuous at limit ordinals.

Cardinal.termℶ_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped notation "ℶ_ " => beth

Beth function notation

Informal description

The notation `ℶ_` is defined as a shorthand for the beth function `beth`, which is a normal function on cardinals satisfying `ℶ_ 0 = 0` and `ℶ_ (succ o) = 2 ^ (ℶ_ o)` for all ordinals `o`. This function enumerates certain large cardinals in set theory.

Cardinal.beth_eq_preBeth theorem

(o : Ordinal) : beth o = preBeth (ω + o)

Full source

theorem beth_eq_preBeth (o : Ordinal) : beth o = preBeth (ω + o) :=
  rfl

$\beth(o) = \text{preBeth}(\omega + o)$

Informal description

For any ordinal $o$, the Beth function $\beth(o)$ is equal to the pre-Beth function evaluated at $\omega + o$, i.e., $\beth(o) = \text{preBeth}(\omega + o)$.

Cardinal.preBeth_le_beth theorem

(o : Ordinal) : preBeth o ≤ ℶ_ o

Full source

theorem preBeth_le_beth (o : Ordinal) : preBeth o ≤ ℶ_ o :=
  preBeth_le_preBeth.2 (Ordinal.le_add_left _ _)

Pre-Beth Function Bounded by Beth Function: $\text{preBeth}(o) \leq \beth(o)$

Informal description

For any ordinal $o$, the pre-Beth function evaluated at $o$ is less than or equal to the Beth function evaluated at $o$, i.e., $\text{preBeth}(o) \leq \beth(o)$.

Cardinal.beth_strictMono theorem

: StrictMono beth

Full source

theorem beth_strictMono : StrictMono beth :=
  preBeth_strictMono.comp fun _ _ h ↦ add_lt_add_left h _

Strict Monotonicity of the Beth Function

Informal description

The Beth function $\beth : \text{Ordinal} \to \text{Cardinal}$ is strictly increasing. That is, for any ordinals $o_1$ and $o_2$, if $o_1 < o_2$, then $\beth(o_1) < \beth(o_2)$.

Cardinal.beth_mono theorem

: Monotone beth

Full source

theorem beth_mono : Monotone beth :=
  beth_strictMono.monotone

Monotonicity of the Beth Function

Informal description

The Beth function $\beth : \text{Ordinal} \to \text{Cardinal}$ is monotone. That is, for any ordinals $o_1$ and $o_2$, if $o_1 \leq o_2$, then $\beth(o_1) \leq \beth(o_2)$.

Cardinal.beth_lt_beth theorem

{o₁ o₂ : Ordinal} : ℶ_ o₁ < ℶ_ o₂ ↔ o₁ < o₂

Full source

@[simp]
theorem beth_lt_beth {o₁ o₂ : Ordinal} : ℶ_ℶ_ o₁ < ℶ_ o₂ ↔ o₁ < o₂ :=
  beth_strictMono.lt_iff_lt

$\beth(o_1) < \beth(o_2) \leftrightarrow o_1 < o_2$

Informal description

For any two ordinals $o_1$ and $o_2$, the Beth cardinal $\beth(o_1)$ is strictly less than $\beth(o_2)$ if and only if $o_1$ is strictly less than $o_2$.

Cardinal.beth_le_beth theorem

{o₁ o₂ : Ordinal} : ℶ_ o₁ ≤ ℶ_ o₂ ↔ o₁ ≤ o₂

Full source

@[simp]
theorem beth_le_beth {o₁ o₂ : Ordinal} : ℶ_ℶ_ o₁ ≤ ℶ_ o₂ ↔ o₁ ≤ o₂ :=
  beth_strictMono.le_iff_le

Monotonicity of Beth Cardinals: $\beth(o₁) \leq \beth(o₂) \leftrightarrow o₁ \leq o₂$

Informal description

For any two ordinals $o₁$ and $o₂$, the Beth cardinal $\beth(o₁)$ is less than or equal to $\beth(o₂)$ if and only if $o₁$ is less than or equal to $o₂$.

Cardinal.beth_zero theorem

: ℶ_ 0 = ℵ₀

Full source

@[simp]
theorem beth_zero : ℶ_ 0 = ℵ₀ := by
  simp [beth]

Beth Function at Zero: $\beth(0) = \aleph_0$

Informal description

The Beth function evaluated at the ordinal $0$ equals the first infinite cardinal $\aleph_0$, i.e., $\beth(0) = \aleph_0$.

Cardinal.beth_succ theorem

(o : Ordinal) : ℶ_ (succ o) = 2 ^ ℶ_ o

Full source

@[simp]
theorem beth_succ (o : Ordinal) : ℶ_ (succ o) = 2 ^ ℶ_ o := by
  simp [beth, add_succ]

Successor Property of Beth Cardinals: $\beth(\operatorname{succ}(o)) = 2^{\beth(o)}$

Informal description

For any ordinal $o$, the Beth cardinal at the successor ordinal $\operatorname{succ}(o)$ is equal to $2$ raised to the power of the Beth cardinal at $o$, i.e., \[ \beth(\operatorname{succ}(o)) = 2^{\beth(o)}. \]

Cardinal.beth_limit theorem

{o : Ordinal} (ho : o.IsLimit) : ℶ_ o = ⨆ a : Iio o, ℶ_ a

Full source

theorem beth_limit {o : Ordinal} (ho : o.IsLimit) : ℶ_ o = ⨆ a : Iio o, ℶ_ a := by
  rw [beth_eq_preBeth, preBeth_limit (isLimit_add ω ho).isSuccPrelimit]
  apply le_antisymm <;>
    apply ciSup_mono' (bddAbove_of_small _) <;>
    intro i
  · refine ⟨⟨_, sub_lt_of_lt_add i.2 ho.pos⟩, ?_⟩
    simpa [beth_eq_preBeth] using le_add_sub _ _
  · exact ⟨⟨_, add_lt_add_left i.2 ω⟩, le_rfl⟩

Limit Property of Beth Cardinals: $\beth(o) = \sup_{a < o} \beth(a)$ for Limit Ordinals $o$

Informal description

For any limit ordinal $o$, the Beth cardinal $\beth(o)$ is equal to the supremum of $\beth(a)$ for all $a < o$, i.e., \[ \beth(o) = \sup_{a < o} \beth(a). \]

Cardinal.aleph_le_beth theorem

(o : Ordinal) : ℵ_ o ≤ ℶ_ o

Full source

theorem aleph_le_beth (o : Ordinal) : ℵ_ o ≤ ℶ_ o :=
  preAleph_le_preBeth _

$\aleph_o \leq \beth_o$ for all ordinals $o$

Informal description

For any ordinal $o$, the $\aleph$ cardinal $\aleph_o$ is less than or equal to the $\beth$ cardinal $\beth_o$, i.e., $\aleph_o \leq \beth_o$.

Cardinal.aleph0_le_beth theorem

(o : Ordinal) : ℵ₀ ≤ ℶ_ o

Full source

theorem aleph0_le_beth (o : Ordinal) : ℵ₀ ≤ ℶ_ o :=
  (aleph0_le_aleph o).trans <| aleph_le_beth o

$\aleph_0 \leq \beth_o$ for all ordinals $o$

Informal description

For any ordinal number $o$, the cardinal $\aleph_0$ is less than or equal to the Beth cardinal $\beth_o$, i.e., $\aleph_0 \leq \beth_o$.

Cardinal.beth_pos theorem

(o : Ordinal) : 0 < ℶ_ o

Full source

theorem beth_pos (o : Ordinal) : 0 < ℶ_ o :=
  aleph0_pos.trans_le <| aleph0_le_beth o

Positivity of Beth cardinals: $0 < \beth_o$ for all ordinals $o$

Informal description

For any ordinal $o$, the Beth cardinal $\beth_o$ is strictly greater than zero, i.e., $0 < \beth_o$.

Cardinal.beth_ne_zero theorem

(o : Ordinal) : ℶ_ o ≠ 0

Full source

theorem beth_ne_zero (o : Ordinal) : ℶ_ℶ_ o ≠ 0 :=
  (beth_pos o).ne'

Nonzero Beth Cardinals: $\beth_o \neq 0$ for all ordinals $o$

Informal description

For any ordinal $o$, the Beth cardinal $\beth_o$ is nonzero, i.e., $\beth_o \neq 0$.

Cardinal.isNormal_beth theorem

: IsNormal (ord ∘ beth)

Full source

theorem isNormal_beth : IsNormal (ordord ∘ beth) :=
  isNormal_preBeth.trans (isNormal_add_right ω)

Normality of the Ordinal Embedding of the Beth Function

Informal description

The composition of the ordinal embedding function $\mathrm{ord}$ with the Beth function $\beth$ is a normal function. That is: 1. It is strictly increasing: for any ordinals $o_1 < o_2$, we have $\mathrm{ord}(\beth(o_1)) < \mathrm{ord}(\beth(o_2))$. 2. It is continuous at limit ordinals: for any limit ordinal $o$, we have $\mathrm{ord}(\beth(o)) = \sup_{a < o} \mathrm{ord}(\beth(a))$.

Cardinal.isStrongLimit_beth theorem

{o : Ordinal} (H : IsSuccPrelimit o) : IsStrongLimit (ℶ_ o)

Full source

theorem isStrongLimit_beth {o : Ordinal} (H : IsSuccPrelimit o) : IsStrongLimit (ℶ_ o) := by
  rcases eq_or_ne o 0 with (rfl | h)
  · rw [beth_zero]
    exact isStrongLimit_aleph0
  · refine ⟨beth_ne_zero o, fun a ha ↦ ?_⟩
    rw [beth_limit] at ha
    · rcases exists_lt_of_lt_ciSup' ha with ⟨⟨i, hi⟩, ha⟩
      have := power_le_power_left two_ne_zero ha.le
      rw [← beth_succ] at this
      exact this.trans_lt (beth_strictMono (H.succ_lt hi))
    · rw [isLimit_iff]
      exact ⟨h, H⟩

Beth Cardinals at Successor Pre-Limit Ordinals are Strong Limit Cardinals

Informal description

For any ordinal $o$ that is a successor pre-limit (i.e., there is no ordinal immediately preceding $o$), the Beth cardinal $\beth(o)$ is a strong limit cardinal. That is, $\beth(o)$ is nonzero and for every cardinal $\kappa < \beth(o)$, we have $2^\kappa < \beth(o)$.