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

• Generalize the universes in the lemmas about iSup, by taking a Small assumption when necessary instead.
• Prove more theorems on inaccessible cardinals.
• Define singular cardinals.

Regular cardinals

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

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

Equations

• c.IsRegular = (Cardinal.aleph0 ≤ c ∧ c ≤ c.ord.cof)

theorem Cardinal.IsRegular.aleph0_le {c : Cardinal.{u_1}} (H : c.IsRegular) : aleph0 ≤ c

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

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}} (h : aleph0 ≤ c) : (Order.succ c).IsRegular

theorem Cardinal.isRegular_aleph_one : (aleph 1).IsRegular

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

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

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

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) : (∀ (i : ι), f i < c.ord) → Ordinal.lsub f < c.ord

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

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) : (∀ (i : ι), f i < c.ord) → iSup f < c.ord

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

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

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

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

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

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) : (∀ (i : ι), f i < c) → iSup f < c

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 {ι : 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

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

@[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 {ι α : Type u} {t : ι → Set α} {c : Cardinal.{u}} (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 {α β : 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

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

Inaccessible cardinals

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

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

Equations

• c.IsInaccessible = (Cardinal.aleph0 < c ∧ c ≤ c.ord.cof ∧ ∀ x < c, 2 ^ x < c)

theorem Cardinal.IsInaccessible.aleph0_lt {c : Cardinal.{u_1}} (h : c.IsInaccessible) : aleph0 < c

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_def {c : Cardinal.{u_1}} : c.IsInaccessible ↔ aleph0 < c ∧ c.IsRegular ∧ c.IsStrongLimit

@[deprecated Cardinal.isInaccessible_def (since := "2025-08-20")]

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

Alias of Cardinal.isInaccessible_def.

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

theorem Ordinal.iSup_sequence_lt_omega_one {α : Type u} [Countable α] (o : α → Ordinal.{max u v}) (ho : ∀ (n : α), o n < (Cardinal.aleph 1).ord) : iSup o < (Cardinal.aleph 1).ord

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

theorem Ordinal.iSup_sequence_lt_omega1 {α : Type u} [Countable α] (o : α → Ordinal.{max u v}) (ho : ∀ (n : α), o n < (Cardinal.aleph 1).ord) : iSup o < (Cardinal.aleph 1).ord

Alias of Ordinal.iSup_sequence_lt_omega_one.