Regular cardinals #

This file defines regular and inaccessible cardinals.

Main definitions #

Cardinal.IsRegular c means that c is a regular cardinal: ℵ₀ ≤ c ∧ c.ord.cof = c.
Cardinal.IsInaccessible c means that c is strongly inaccessible: ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c.

TODO #

Prove more theorems on inaccessible cardinals.
Define singular cardinals.

Regular cardinals #

source

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.

Instances For

source

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

c.ord.cof = c

source

@[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.

source

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

(Ordinal.omega o).cof = aleph o

source

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

0 < c

source

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

↑n < c

source

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

0 < c.ord

source

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

o.cof.IsRegular

source

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.

source

theorem Cardinal.isRegular_aleph0 :

aleph0.IsRegular

source

theorem Cardinal.fact_isRegular_aleph0 :

Fact aleph0.IsRegular

source

theorem Cardinal.isRegular_succ {c : Cardinal.{u}} (h : aleph0 ≤ c) :

(Order.succ c).IsRegular

source

theorem Cardinal.isRegular_aleph_one :

(aleph 1).IsRegular

source

@[simp]

theorem Cardinal.cof_omega_one :

(Ordinal.omega 1).cof = aleph 1

source

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.

source

@[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.

source

@[deprecated Ordinal.iSup_lt_omega_one (since := "2025-12-22")]

theorem Cardinal.iSup_sequence_lt_omega1 {α : 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.

source

theorem Cardinal.isRegular_preAleph_add_one {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) :

(preAleph (o + 1)).IsRegular

source

@[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

source

theorem Cardinal.cof_preOmega_add_one {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) :

(Ordinal.preOmega (o + 1)).cof = preAleph (o + 1)

source

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

(aleph (o + 1)).IsRegular

source

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

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

(aleph (Order.succ o)).IsRegular

source

@[simp]

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

(Ordinal.omega (o + 1)).cof = aleph (o + 1)

source

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

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

source

@[simp]

theorem Cardinal.isRegular_lift_iff {κ : Cardinal.{v}} :

(lift.{u, v} κ).IsRegular ↔ κ.IsRegular

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[deprecated Ordinal.lift_iSup_lt_of_lt_cof (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

source

@[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

source

theorem Cardinal.sum_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) :

sum f < c

source

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

(∀ (i : ι), f i < c) → sum f < c

source

@[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

source

@[simp]

theorem Cardinal.card_iUnion_lt_iff_forall_of_isRegular {ι α : Type u} {t : ι → Set α} {c : Cardinal.{u}} (hc : c.IsRegular) (hι : mk ι < c) :

mk ↑(⋃ (i : ι), t i) < c ↔ ∀ (i : ι), mk ↑(t i) < c

source

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

source

theorem Cardinal.card_biUnion_lt_iff_forall_of_isRegular {α β : Type u} {s : Set α} {t : (a : α) → a ∈ s → Set β} {c : Cardinal.{u}} (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

source

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

source

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

source

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

source

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

source

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

source

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

Inaccessible cardinals #

source

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.
two_power_lt ⦃x : Cardinal.{u_1}⦄ : x < c → 2 ^ x < c
An inaccessible cardinal is a strong limit, see IsInaccessible.isStrongLimit.