Regular cardinals

This file defines regular, singular, and inaccessible cardinals.

Main definitions

• Cardinal.IsRegular c means that c is an infinite cardinal, equal to its own cofinality.
• Cardinal.IsSingular c means that c is an infinite cardinal which is not regular. That is, its cofinality is smaller than itself.
• Cardinal.IsInaccessible c means that c is strongly inaccessible: ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c.

Regular cardinals

structure Cardinal.IsRegular (c : Cardinal.{u_1}) : Prop

A cardinal is regular if it is infinite and it equals its own cofinality.

• aleph0_le : aleph0 ≤ c

  A regular cardinal is infinite.

• le_cof_ord : c ≤ c.ord.cof

  A cardinal equals its own cofinality. See IsRegular.cof_eq.

theorem Cardinal.isRegular_iff (c : Cardinal.{u_1}) : c.IsRegular ↔ aleph0 ≤ c ∧ c ≤ c.ord.cof

theorem Cardinal.IsRegular.cof_ord {c : Cardinal.{u_1}} (H : c.IsRegular) : c.ord.cof = c

@[deprecated Cardinal.IsRegular.cof_ord (since := "2026-03-22")]

theorem Cardinal.IsRegular.cof_eq {c : Cardinal.{u_1}} (H : c.IsRegular) : c.ord.cof = c

Alias of Cardinal.IsRegular.cof_ord.

theorem Cardinal.IsRegular.cof_omega_eq {o : Ordinal.{u_1}} (H : (aleph o).IsRegular) : (Ordinal.omega o).cof = aleph o

theorem Cardinal.IsRegular.pos {c : Cardinal.{u_1}} (H : c.IsRegular) : 0 < c

theorem Cardinal.IsRegular.nat_lt {c : Cardinal.{u_1}} (H : c.IsRegular) (n : ℕ) : ↑n < c

theorem Cardinal.IsRegular.ord_pos {c : Cardinal.{u_1}} (H : c.IsRegular) : 0 < c.ord

theorem Cardinal.isRegular_cof {o : Ordinal.{u_1}} (h : Order.IsSuccLimit o) : o.cof.IsRegular

theorem Cardinal.IsRegular.ne_zero {c : Cardinal.{u_1}} (H : c.IsRegular) : c ≠ 0

If c is a regular cardinal, then c.ord.ToType has a least element.

theorem Cardinal.isRegular_aleph0 : aleph0.IsRegular

theorem Cardinal.fact_isRegular_aleph0 : Fact aleph0.IsRegular

theorem Cardinal.isRegular_succ {c : Cardinal.{u_1}} (hc : aleph0 ≤ c) : (Order.succ c).IsRegular

theorem Cardinal.isRegular_aleph_one : (aleph 1).IsRegular

@[simp]

theorem Cardinal.cof_omega_one : (Ordinal.omega 1).cof = aleph 1

theorem Ordinal.iSup_lt_omega_one {α : Type u_1} [Countable α] {f : α → Ordinal.{u_2}} : (∀ (i : α), f i < omega 1) → ⨆ (i : α), f i < omega 1

A countable supremum of countable ordinals is countable.

@[deprecated Ordinal.iSup_lt_omega_one (since := "2026-03-23")]

theorem Cardinal.iSup_sequence_lt_omega_one {α : Type u_1} [Countable α] {f : α → Ordinal.{u_2}} : (∀ (i : α), f i < Ordinal.omega 1) → ⨆ (i : α), f i < Ordinal.omega 1

Alias of Ordinal.iSup_lt_omega_one.

---

A countable supremum of countable ordinals is countable.

theorem Cardinal.isRegular_preAleph_add_one {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) : (preAleph (o + 1)).IsRegular

@[deprecated Cardinal.isRegular_preAleph_add_one (since := "2026-03-23")]

theorem Cardinal.isRegular_preAleph_succ {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) : (preAleph (Order.succ o)).IsRegular

theorem Cardinal.cof_preOmega_add_one {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) : (Ordinal.preOmega (o + 1)).cof = preAleph (o + 1)

theorem Cardinal.isRegular_aleph_add_one (o : Ordinal.{u_1}) : (aleph (o + 1)).IsRegular

@[deprecated Cardinal.isRegular_aleph_add_one (since := "2026-03-23")]

theorem Cardinal.isRegular_aleph_succ (o : Ordinal.{u_1}) : (aleph (Order.succ o)).IsRegular

@[simp]

theorem Cardinal.cof_omega_add_one (o : Ordinal.{u_1}) : (Ordinal.omega (o + 1)).cof = aleph (o + 1)

theorem Cardinal.IsRegular.lift {κ : Cardinal.{v}} (h : κ.IsRegular) : (Cardinal.lift.{u, v} κ).IsRegular

@[simp]

theorem Cardinal.isRegular_lift_iff {κ : Cardinal.{v}} : (lift.{u, v} κ).IsRegular ↔ κ.IsRegular

@[deprecated Ordinal.lift_iSup_add_one_lt_of_lt_cof (since := "2026-03-22")]

theorem Cardinal.lsub_lt_ord_lift_of_isRegular {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Cardinal.{max u v}} (hc : c.IsRegular) (hι : lift.{v, u} (mk ι) < c) (hf : ∀ (i : ι), f i < c.ord) : Ordinal.lsub f < c.ord

@[deprecated Ordinal.iSup_add_one_lt_of_lt_cof (since := "2026-03-22")]

theorem Cardinal.lsub_lt_ord_of_isRegular {ι : Type (max u_1 u_2)} {f : ι → Ordinal.{max u_1 u_2}} {c : Cardinal.{max u_1 u_2}} (hc : c.IsRegular) (hι : mk ι < c) : (∀ (i : ι), f i < c.ord) → Ordinal.lsub f < c.ord

@[deprecated Ordinal.lift_iSup_lt_of_lt_cof (since := "2026-03-22")]

theorem Cardinal.iSup_lt_ord_lift_of_isRegular {ι : Type u} {f : ι → Ordinal.{max u v}} {c : Cardinal.{max u v}} (hc : c.IsRegular) (hι : lift.{v, u} (mk ι) < c) (hf : ∀ (i : ι), f i < c.ord) : iSup f < c.ord

@[deprecated Ordinal.iSup_lt_of_lt_cof (since := "2026-03-22")]

theorem Cardinal.iSup_lt_ord_of_isRegular {ι : Type u_1} {f : ι → Ordinal.{u_1}} {c : Cardinal.{u_1}} (hc : c.IsRegular) (hι : mk ι < c) : (∀ (i : ι), f i < c.ord) → iSup f < c.ord

@[deprecated Ordinal.lift_iSup_add_one_lt_of_lt_cof (since := "2026-03-22")]

theorem Cardinal.blsub_lt_ord_lift_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Cardinal.{max u v}} (hc : c.IsRegular) (ho : lift.{v, u} o.card < c) : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord

@[deprecated Ordinal.lift_iSup_add_one_lt_of_lt_cof (since := "2026-03-22")]

theorem Cardinal.blsub_lt_ord_of_isRegular {o : Ordinal.{max u_1 u_2}} {f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}} {c : Cardinal.{max u_1 u_2}} (hc : c.IsRegular) (ho : o.card < c) : (∀ (i : Ordinal.{max u_1 u_2}) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord

@[deprecated Cardinal.iSup_lt_ord_lift_of_isRegular (since := "2026-03-22")]

theorem Cardinal.bsup_lt_ord_lift_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Cardinal.{max u v}} (hc : c.IsRegular) (hι : lift.{v, u} o.card < c) : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord

@[deprecated Ordinal.lift_iSup_lt_of_lt_cof (since := "2026-03-22")]

theorem Cardinal.bsup_lt_ord_of_isRegular {o : Ordinal.{max u_1 u_2}} {f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}} {c : Cardinal.{max u_1 u_2}} (hc : c.IsRegular) (hι : o.card < c) : (∀ (i : Ordinal.{max u_1 u_2}) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord

@[deprecated Cardinal.lift_iSup_lt_of_lt_cof_ord (since := "2026-03-22")]

theorem Cardinal.iSup_lt_lift_of_isRegular {ι : Type u} {f : ι → Cardinal.{max u v}} {c : Cardinal.{max u v}} (hc : c.IsRegular) (hι : lift.{v, u} (mk ι) < c) (hf : ∀ (i : ι), f i < c) : iSup f < c

@[deprecated Ordinal.iSup_lt_of_lt_cof (since := "2026-03-22")]

theorem Cardinal.iSup_lt_of_isRegular {ι : Type u_1} {f : ι → Cardinal.{u_1}} {c : Cardinal.{u_1}} (hc : c.IsRegular) (hι : mk ι < c) : (∀ (i : ι), f i < c) → iSup f < c

theorem Cardinal.sum_lt_lift_of_isRegular {c : Cardinal.{max u v}} {ι : Type u} {f : ι → Cardinal.{max u v}} (hc : c.IsRegular) (hι : lift.{v, u} (mk ι) < c) (hf : ∀ (i : ι), f i < c) : sum f < c

theorem Cardinal.sum_lt_of_isRegular {c : Cardinal.{u}} {ι : Type u} {f : ι → Cardinal.{u}} (hc : c.IsRegular) (hι : mk ι < c) : (∀ (i : ι), f i < c) → sum f < c

@[simp]

theorem Cardinal.card_lt_of_card_iUnion_lt {ι α : Type u} {t : ι → Set α} {c : Cardinal.{u}} (h : mk ↑(⋃ (i : ι), t i) < c) (i : ι) : mk ↑(t i) < c

@[simp]

theorem Cardinal.card_iUnion_lt_iff_forall_of_isRegular {c : Cardinal.{u}} {ι α : Type u} {t : ι → Set α} (hc : c.IsRegular) (hι : mk ι < c) : mk ↑(⋃ (i : ι), t i) < c ↔ ∀ (i : ι), mk ↑(t i) < c

theorem Cardinal.card_lt_of_card_biUnion_lt {α β : Type u} {s : Set α} {t : (a : α) → a ∈ s → Set β} {c : Cardinal.{u}} (h : mk ↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) < c) (a : α) (ha : a ∈ s) : mk ↑(t a ha) < c

theorem Cardinal.card_biUnion_lt_iff_forall_of_isRegular {c : Cardinal.{u}} {α β : Type u} {s : Set α} {t : (a : α) → a ∈ s → Set β} (hc : c.IsRegular) (hs : mk ↑s < c) : mk ↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) < c ↔ ∀ (a : α) (ha : a ∈ s), mk ↑(t a ha) < c

theorem Cardinal.nfpFamily_lt_ord_lift_of_isRegular {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Cardinal.{max u v}} (hc : c.IsRegular) (hι : lift.{v, u} (mk ι) < c) (hc' : c ≠ aleph0) (hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord) {a : Ordinal.{max u v}} (ha : a < c.ord) : Ordinal.nfpFamily f a < c.ord

theorem Cardinal.nfpFamily_lt_ord_of_isRegular {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : mk ι < c) (hc' : c ≠ aleph0) {a : Ordinal.{u}} (hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord) : a < c.ord → Ordinal.nfpFamily f a < c.ord

theorem Cardinal.nfp_lt_ord_of_isRegular {f : Ordinal.{u_1} → Ordinal.{u_1}} {c : Cardinal.{u_1}} (hc : c.IsRegular) (hc' : c ≠ aleph0) (hf : ∀ i < c.ord, f i < c.ord) {a : Ordinal.{u_1}} : a < c.ord → Ordinal.nfp f a < c.ord

theorem Cardinal.derivFamily_lt_ord_lift {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Cardinal.{max u v}} (hc : c.IsRegular) (hι : lift.{v, u} (mk ι) < c) (hc' : c ≠ aleph0) (hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord) {a : Ordinal.{max u v}} : a < c.ord → Ordinal.derivFamily f a < c.ord

theorem Cardinal.derivFamily_lt_ord {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : mk ι < c) (hc' : c ≠ aleph0) (hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord) {a : Ordinal.{u}} : a < c.ord → Ordinal.derivFamily f a < c.ord

theorem Cardinal.deriv_lt_ord {f : Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : c.IsRegular) (hc' : c ≠ aleph0) (hf : ∀ i < c.ord, f i < c.ord) {a : Ordinal.{u}} : a < c.ord → Ordinal.deriv f a < c.ord

Singular cardinals

structure Cardinal.IsSingular (c : Cardinal.{u_1}) : Prop

A cardinal is singular if it is infinite and not regular.

• aleph0_le : aleph0 ≤ c

  A singular cardinal is infinite.

• cof_ord_ne : c.ord.cof ≠ c

  A singular cardinal is not regular, see IsSingular.not_isRegular.

theorem Cardinal.isSingular_iff (c : Cardinal.{u_1}) : c.IsSingular ↔ aleph0 ≤ c ∧ c.ord.cof ≠ c

theorem Cardinal.IsSingular.cof_ord_lt {c : Cardinal.{u_1}} (hc : c.IsSingular) : c.ord.cof < c

theorem Cardinal.IsSingular.natCast_lt {c : Cardinal.{u_1}} (hc : c.IsSingular) (n : ℕ) : ↑n < c

theorem Cardinal.IsSingular.pos {c : Cardinal.{u_1}} (hc : c.IsSingular) : 0 < c

theorem Cardinal.IsSingular.not_isRegular {c : Cardinal.{u_1}} (hc : c.IsSingular) : ¬c.IsRegular

theorem Cardinal.IsRegular.not_isSingular {c : Cardinal.{u_1}} (hc : c.IsRegular) : ¬c.IsSingular

@[simp]

theorem Cardinal.not_isSingular_aleph0 : ¬aleph0.IsSingular

@[simp]

theorem Cardinal.not_isSingular_aleph_one : ¬(aleph 1).IsSingular

@[simp]

theorem Cardinal.not_isSingular_succ (c : Cardinal.{u_1}) : ¬(Order.succ c).IsSingular

@[simp]

theorem Cardinal.not_isRegular_aleph_add_one (o : Ordinal.{u_1}) : ¬(aleph (o + 1)).IsSingular

theorem Cardinal.IsSingular.isSuccLimit {c : Cardinal.{u_1}} (hc : c.IsSingular) : Order.IsSuccLimit c

theorem Cardinal.isRegular_or_isSingular {c : Cardinal.{u_1}} (h : aleph0 ≤ c) : c.IsRegular ∨ c.IsSingular

theorem Cardinal.lt_aleph0_or_isRegular_or_isSingular {c : Cardinal.{u_1}} : c < aleph0 ∨ c.IsRegular ∨ c.IsSingular

theorem Cardinal.IsSingular.of_not_isRegular {c : Cardinal.{u_1}} (h₀ : aleph0 ≤ c) (hc : ¬c.IsRegular) : c.IsSingular

theorem Cardinal.IsRegular.of_not_isSingular {c : Cardinal.{u_1}} (h₀ : aleph0 ≤ c) (hc : ¬c.IsSingular) : c.IsRegular

theorem Cardinal.isSingular_aleph_iff {o : Ordinal.{u_1}} : (aleph o).IsSingular ↔ Order.IsSuccLimit o ∧ o.cof < aleph o

theorem Cardinal.IsSingular.isSuccLimit_of_aleph {o : Ordinal.{u_1}} (hc : (aleph o).IsSingular) : Order.IsSuccLimit o

theorem Cardinal.isSingular_aleph_omega0 : (aleph Ordinal.omega0).IsSingular

theorem Cardinal.IsSingular.aleph_omega0_le {c : Cardinal.{u_1}} (hc : c.IsSingular) : aleph Ordinal.omega0 ≤ c

Inaccessible cardinals

structure Cardinal.IsInaccessible (c : Cardinal.{u_1}) : Prop

A cardinal is inaccessible if it is an uncountable regular strong limit cardinal.

• aleph0_lt : aleph0 < c

  An inaccessible cardinal is uncountable.

• le_cof_ord : c ≤ c.ord.cof

  An inaccessible cardinal is equal to its own cofinality, see IsInaccessible.isRegular.

• isStrongPrelimit : c.IsStrongPrelimit

  An inaccessible cardinal is a strong limit, see IsInaccessible.isStrongLimit.

theorem Cardinal.IsInaccessible.nat_lt {c : Cardinal.{u_1}} (h : c.IsInaccessible) (n : ℕ) : ↑n < c

theorem Cardinal.IsInaccessible.pos {c : Cardinal.{u_1}} (h : c.IsInaccessible) : 0 < c

theorem Cardinal.IsInaccessible.ne_zero {c : Cardinal.{u_1}} (h : c.IsInaccessible) : c ≠ 0

theorem Cardinal.IsInaccessible.isRegular {c : Cardinal.{u_1}} (h : c.IsInaccessible) : c.IsRegular

theorem Cardinal.IsInaccessible.isStrongLimit {c : Cardinal.{u_1}} (h : c.IsInaccessible) : c.IsStrongLimit

theorem Cardinal.IsInaccessible.isSuccLimit {c : Cardinal.{u_1}} (h : c.IsInaccessible) : Order.IsSuccLimit c

theorem Cardinal.isInaccessible_def {c : Cardinal.{u_1}} : c.IsInaccessible ↔ aleph0 < c ∧ c.IsRegular ∧ c.IsStrongLimit

theorem Cardinal.IsInaccessible.univ : Cardinal.univ.{u, v}.IsInaccessible

Lean's foundations prove the existence of v inaccessibles in universe v.

theorem Cardinal.IsInaccessible.preBeth_ord {c : Cardinal.{u_1}} (hc : c.IsInaccessible) : preBeth c.ord = c

theorem Cardinal.IsInaccessible.beth_ord {c : Cardinal.{u_1}} (hc : c.IsInaccessible) : beth c.ord = c

theorem Cardinal.IsInaccessible.preAleph_ord {c : Cardinal.{u_1}} (hc : c.IsInaccessible) : preAleph c.ord = c

theorem Cardinal.IsInaccessible.preAleph_symm_eq_ord {c : Cardinal.{u_1}} (hc : c.IsInaccessible) : preAleph.symm c = c.ord

theorem Cardinal.IsInaccessible.aleph_ord {c : Cardinal.{u_1}} (hc : c.IsInaccessible) : aleph c.ord = c

theorem Cardinal.IsInaccessible.preOmega_ord {c : Cardinal.{u_1}} (hc : c.IsInaccessible) : Ordinal.preOmega c.ord = c.ord

theorem Cardinal.IsInaccessible.omega_ord {c : Cardinal.{u_1}} (hc : c.IsInaccessible) : Ordinal.omega c.ord = c.ord

@[simp]

theorem Cardinal.preBeth_univ : preBeth Ordinal.univ.{u, v} = univ.{u, v}

@[simp]

theorem Cardinal.beth_univ : beth Ordinal.univ.{u, v} = univ.{u, v}

@[simp]

theorem Cardinal.preAleph_univ : preAleph Ordinal.univ.{u, v} = univ.{u, v}

@[simp]

theorem Cardinal.preAleph_symm_univ : preAleph.symm univ.{u, v} = Ordinal.univ.{u, v}

@[simp]

theorem Cardinal.aleph_univ : aleph Ordinal.univ.{u, v} = univ.{u, v}

@[simp]

theorem Ordinal.preOmega_univ : preOmega univ.{u, v} = univ.{u, v}

@[simp]

theorem Ordinal.omega_univ : omega univ.{u, v} = univ.{u, v}