Aleph and beth functions

• The function Cardinal.aleph' gives the cardinals listed by their ordinal index. aleph' n = n, aleph' ω = ℵ₀, aleph' (ω + 1) = succ ℵ₀, etc. It is an order isomorphism between ordinals and cardinals.
• The function Cardinal.aleph gives the infinite cardinals listed by their ordinal index. aleph 0 = ℵ₀, aleph 1 = succ ℵ₀ is the first uncountable cardinal, and so on. The notation ω_ combines the latter with Cardinal.ord, giving an enumeration of (infinite) initial ordinals. Thus ω_ 0 = ω and ω₁ = ω_ 1 is the first uncountable ordinal.
• The function Cardinal.beth enumerates the Beth cardinals. beth 0 = ℵ₀, beth (succ o) = 2 ^ beth o, and for a limit ordinal o, beth o is the supremum of beth a for a < o.

Notation

The following notation is scoped to the Cardinal namespace.

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

Omega ordinals

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)

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

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

theorem Ordinal.IsInitial.card_lt_card {a : Ordinal.{u_1}} {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 : Ordinal.IsInitial 0

theorem Ordinal.isInitial_one : Ordinal.IsInitial 1

theorem Ordinal.isInitial_omega0 : Ordinal.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_symm_apply_coe (x : Cardinal.{u_1}) : ↑((RelIso.symm Ordinal.isInitialIso) x) = x.ord

@[simp]

theorem Ordinal.isInitialIso_apply (x : { x : Ordinal.{u_1} // x.IsInitial }) : Ordinal.isInitialIso x = (↑x).card

Aleph cardinals

def Cardinal.aleph' : Ordinal.{u} ≃o Cardinal.{u}

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

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

Equations

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

@[deprecated Cardinal.aleph']

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

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

Equations

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

@[deprecated Cardinal.aleph']

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

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

Equations

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

@[deprecated Cardinal.aleph']

def Cardinal.alephIdx : Cardinal.{u_1} → Ordinal.{u_1}

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ω = ω, alephIdx ℵ₁ = ω + 1 and so on.) For an upgraded version stating that the range is everything, see AlephIdx.rel_iso.

Equations

• Cardinal.alephIdx = ⇑Cardinal.aleph'.symm

@[deprecated]

theorem Cardinal.alephIdx.initialSeg_coe : ⇑Cardinal.alephIdx.initialSeg = Cardinal.alephIdx

@[deprecated]

theorem Cardinal.alephIdx_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} : a.alephIdx < b.alephIdx ↔ a < b

@[deprecated]

theorem Cardinal.alephIdx_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} : a.alephIdx ≤ b.alephIdx ↔ a ≤ b

@[deprecated]

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

@[deprecated]

theorem Cardinal.alephIdx.relIso_coe : ⇑Cardinal.alephIdx.relIso = Cardinal.alephIdx

@[simp]

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

@[simp]

theorem Cardinal.mk_cardinal : Cardinal.mk Cardinal.{u} = Cardinal.univ.{u, u + 1}

@[deprecated Cardinal.aleph']

def Cardinal.Aleph'.relIso : Ordinal.{u_1} ≃o Cardinal.{u_1}

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

Equations

• Cardinal.Aleph'.relIso = Cardinal.aleph'

@[deprecated]

theorem Cardinal.aleph'.relIso_coe : ⇑Cardinal.Aleph'.relIso = ⇑Cardinal.aleph'

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

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

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

@[deprecated]

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

@[deprecated]

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

@[simp]

theorem Cardinal.aleph'_zero : Cardinal.aleph' 0 = 0

@[simp]

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

@[simp]

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

theorem Cardinal.aleph'_le_of_limit {o : Ordinal.{u_1}} (l : o.IsLimit) {c : Cardinal.{u_1}} : Cardinal.aleph' o ≤ c ↔ ∀ o' < o, Cardinal.aleph' o' ≤ c

theorem Cardinal.aleph'_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) : Cardinal.aleph' o = ⨆ (a : ↑(Set.Iio o)), Cardinal.aleph' ↑a

@[simp]

theorem Cardinal.aleph'_omega0 : Cardinal.aleph' Ordinal.omega0 = Cardinal.aleph0

@[deprecated Cardinal.aleph'_omega0]

theorem Cardinal.aleph'_omega : Cardinal.aleph' Ordinal.omega0 = Cardinal.aleph0

Alias of Cardinal.aleph'_omega0.

@[deprecated Cardinal.aleph']

def Cardinal.aleph'Equiv : Ordinal.{u_1} ≃ Cardinal.{u_1}

aleph' and aleph_idx form an equivalence between Ordinal and Cardinal

Equations

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

def Cardinal.aleph : Ordinal.{u_1} ↪o Cardinal.{u_1}

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

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

Equations

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

theorem Cardinal.aleph_eq_aleph' (o : Ordinal.{u_1}) : Cardinal.aleph o = Cardinal.aleph' (Ordinal.omega0 + o)

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

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

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

@[deprecated Cardinal.aleph_max]

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

@[simp]

theorem Cardinal.aleph_succ (o : Ordinal.{u_1}) : Cardinal.aleph (Order.succ o) = Order.succ (Cardinal.aleph o)

@[simp]

theorem Cardinal.aleph_zero : Cardinal.aleph 0 = Cardinal.aleph0

theorem Cardinal.aleph_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) : Cardinal.aleph o = ⨆ (a : ↑(Set.Iio o)), Cardinal.aleph ↑a

theorem Cardinal.aleph0_le_aleph' {o : Ordinal.{u_1}} : Cardinal.aleph0 ≤ Cardinal.aleph' o ↔ Ordinal.omega0 ≤ o

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

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

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

@[simp]

theorem Cardinal.aleph_toNat (o : Ordinal.{u_1}) : Cardinal.toNat (Cardinal.aleph o) = 0

@[simp]

theorem Cardinal.aleph_toPartENat (o : Ordinal.{u_1}) : Cardinal.toPartENat (Cardinal.aleph o) = ⊤

instance Cardinal.nonempty_toType_aleph (o : Ordinal.{u_1}) : Nonempty (Cardinal.aleph o).ord.toType

Equations

• ⋯ = ⋯

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

instance Cardinal.instNoMaxOrderToTypeOrdCoeOrderEmbeddingOrdinalAleph (o : Ordinal.{u_1}) : NoMaxOrder (Cardinal.aleph o).ord.toType

Equations

• ⋯ = ⋯

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

theorem Cardinal.aleph'_isNormal : Ordinal.IsNormal (Cardinal.ord ∘ ⇑Cardinal.aleph')

theorem Cardinal.aleph_isNormal : Ordinal.IsNormal (Cardinal.ord ∘ ⇑Cardinal.aleph)

theorem Cardinal.succ_aleph0 : Order.succ Cardinal.aleph0 = Cardinal.aleph 1

theorem Cardinal.aleph0_lt_aleph_one : Cardinal.aleph0 < Cardinal.aleph 1

theorem Cardinal.countable_iff_lt_aleph_one {α : Type u_1} (s : Set α) : s.Countable ↔ Cardinal.mk ↑s < Cardinal.aleph 1

@[deprecated]

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

Ordinals that are cardinals are unbounded.

@[deprecated]

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

@[deprecated]

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

Infinite ordinals that are cardinals are unbounded.

@[deprecated]

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

Beth cardinals

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

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

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

Equations

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

@[simp]

theorem Cardinal.beth_zero : Cardinal.beth 0 = Cardinal.aleph0

@[simp]

theorem Cardinal.beth_succ (o : Ordinal.{u_1}) : Cardinal.beth (Order.succ o) = 2 ^ Cardinal.beth o

theorem Cardinal.beth_limit {o : Ordinal.{u_1}} : o.IsLimit → Cardinal.beth o = ⨆ (a : ↑(Set.Iio o)), Cardinal.beth ↑a

theorem Cardinal.beth_strictMono : StrictMono Cardinal.beth

theorem Cardinal.beth_mono : Monotone Cardinal.beth

@[simp]

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

@[simp]

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

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

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

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

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

theorem Cardinal.isNormal_beth : Ordinal.IsNormal (Cardinal.ord ∘ Cardinal.beth)

@[deprecated Cardinal.isNormal_beth]

theorem Cardinal.beth_normal : Ordinal.IsNormal fun (o : Ordinal.{u}) => (Cardinal.beth o).ord

Omega ordinals

theorem Ordinal.omega_lt_omega1 : Ordinal.omega0 < (Cardinal.aleph 1).ord