# 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 #

source
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)

Instances For

source
theorem Cardinal.IsRegular.aleph0_le {c : Cardinal.{u_1}} (H : c.IsRegular) :
aleph0 ≤ c
source
theorem Cardinal.IsRegular.cof_eq {c : Cardinal.{u_1}} (H : c.IsRegular) :
c.ord.cof = c
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
theorem Cardinal.isRegular_preAleph_succ {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) :
(preAleph (Order.succ o)).IsRegular
source
theorem Cardinal.isRegular_aleph_succ (o : Ordinal.{u_1}) :
(aleph (Order.succ o)).IsRegular
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
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
source
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
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
source
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
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
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
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
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
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
source
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
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)

Instances For

source
@[deprecated "use the default constructor for `IsInaccessible`" (since := "2025-07-01")]
theorem Cardinal.IsInaccessible.mk {c : Cardinal.{u_1}} (h₁ : aleph0 < c) (h₂ : c ≤ c.ord.cof) (h₃ : ∀ x < c, 2 ^ x < c) :
c.IsInaccessible
source
theorem Cardinal.IsInaccessible.aleph0_lt {c : Cardinal.{u_1}} (h : c.IsInaccessible) :
aleph0 < c
source
theorem Cardinal.IsInaccessible.nat_lt {c : Cardinal.{u_1}} (h : c.IsInaccessible) (n : ℕ) :
↑n < c
source
theorem Cardinal.IsInaccessible.pos {c : Cardinal.{u_1}} (h : c.IsInaccessible) :
0 < c
source
theorem Cardinal.IsInaccessible.ne_zero {c : Cardinal.{u_1}} (h : c.IsInaccessible) :
c ≠ 0
source
theorem Cardinal.IsInaccessible.isRegular {c : Cardinal.{u_1}} (h : c.IsInaccessible) :
c.IsRegular
source
theorem Cardinal.IsInaccessible.isStrongLimit {c : Cardinal.{u_1}} (h : c.IsInaccessible) :
c.IsStrongLimit
source
theorem Cardinal.isInaccessible_def {c : Cardinal.{u_1}} :
c.IsInaccessible ↔ aleph0 < c ∧ c.IsRegular ∧ c.IsStrongLimit
source
@[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`.

source
theorem Cardinal.IsInaccessible.univ :
Cardinal.univ.{u, v}.IsInaccessible
source
@[deprecated Cardinal.IsInaccessible.univ (since := "2025-07-01")]
theorem Cardinal.univ_inaccessible :
univ.{u, v}.IsInaccessible

Alias of `Cardinal.IsInaccessible.univ`.

source
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