Inaccessible cardinals

DefinitionWeakly inaccessible cardinal#✓fully proved

A cardinal κ is weakly inaccessible if it is an uncountable, regular limit cardinal.

def IsWeaklyInaccessible.{u} (κ : Cardinal.{u}) : Prop :=
  ℵ₀ < κ ∧ κ.IsRegular ∧ Order.IsSuccLimit κ

Used by 3

Used byLimit cardinals are unbounded below a weakly inaccessible cardinal · Under GCH, weakly inaccessible cardinals are inaccessible · Weakly Mahlo cardinal

DefinitionSet of inaccessible cardinals below a cardinal#✓fully proved

InAccBelow κ is the set of all inaccessible cardinals below κ.

def inaccessibleBelow.{u} (κ : Cardinal.{u}) : Set (Set.Iio κ.ord) :=
  {α | Cardinal.IsInaccessible α.val.card ∧ α.val.card.ord = α.val}

Used by 6

Used byAt most \(\kappa\) inaccessible cardinals lie below \(\kappa\) · Exactly \(\kappa\) inaccessibles lie below an inaccessible fixed point · Existence of an inaccessible with no inaccessibles below it · Inaccessible fixed point · Inaccessibles are unbounded below an inaccessible fixed point · Mahlo cardinal

DefinitionInaccessible fixed point#✓fully proved

A cardinal κ is an inaccessible fixed point if κ is inaccessible and the inaccessibles below κ have order type κ (i.e. κ is the κ-th inaccessible).

def IsInaccessibleFixedPoint.{u} (κ : Cardinal.{u}) : Prop :=
  Cardinal.IsInaccessible κ ∧
  Ordinal.lift.{u+1} κ.ord = typeLT ↥(inaccessibleBelow κ)

Uses 1 · Used by 2

Statement usesSet of inaccessible cardinals below a cardinal

Used byExactly \(\kappa\) inaccessibles lie below an inaccessible fixed point · Inaccessibles are unbounded below an inaccessible fixed point

TheoremThe beth hierarchy stays below an inaccessible cardinal#✓fully proved

Below an inaccessible κ, the beth hierarchy stays below κ: κ is a beth fixed point (IsInaccessible.beth_ord) and beth is strictly monotone.

theorem _root_.Cardinal.IsInaccessible.beth_lt.{u} {κ : Cardinal.{u}} (hκ : κ.IsInaccessible)
    {o : Ordinal.{u}} (ho : o < κ.ord) : (ℶ_ o : Cardinal.{u}) < κ

Sources

• Below an inaccessible κ, each ℶ_o with o < κ.ord lies below κ.

Used by 1

Used byStrong limits are unbounded below an inaccessible cardinal

TheoremThe aleph hierarchy stays below an inaccessible cardinal#✓fully proved

Below an inaccessible κ, the aleph hierarchy stays below κ: same argument via IsInaccessible.aleph_ord.

theorem Cardinal.IsInaccessible.aleph_lt.{u} {κ : Cardinal.{u}} (hκ : κ.IsInaccessible)
    {o : Ordinal.{u}} (ho : o < κ.ord) : (ℵ_ o : Cardinal.{u}) < κ

Sources

• Below an inaccessible κ, each ℵ_o with o < κ.ord lies below κ.

TheoremAt most \(\kappa\) inaccessible cardinals lie below \(\kappa\)#✓fully proved

There are at most κ inaccessibles below κ: the set injects into ↥(Set.Iio κ.ord), which has size lift κ. The ≤ half of the counting needed for the Mahlo-implies-fixed-point benchmark item.

The lift is forced: the carrier lives in Type (u+1), the same phenomenon as the lift in IsInaccessibleFixedPoint.

theorem mk_inaccessibleBelow_le.{u} (κ : Cardinal.{u}) :
    #(↥(inaccessibleBelow κ)) ≤ Cardinal.lift.{u+1} κ

Sources

• There are at most κ inaccessible cardinals below κ.

Uses 1

Statement usesSet of inaccessible cardinals below a cardinal

TheoremRegular cardinals are unbounded below an uncountable limit cardinal#✓fully proved

Regular cardinals are unbounded below an uncountable limit cardinal κ (in particular a weakly inaccessible one): above any a < κ sits succ (max a ℵ₀), regular by isRegular_succ and below κ since κ is a limit.

theorem exists_regular_between.{u} {κ : Cardinal.{u}} (hlt : ℵ₀ < κ)
    (hlim : Order.IsSuccLimit κ) {a : Cardinal.{u}} (ha : a < κ) :
    ∃ r : Cardinal.{u}, a < r ∧ r < κ ∧ r.IsRegular

Sources

• Regular cardinals are unbounded below any uncountable limit cardinal.

TheoremUnder GCH, weakly inaccessible cardinals are inaccessible#✓fully proved

Under (local) GCH, weakly inaccessible implies strongly inaccessible: for infinite μ < κ, 2 ^ μ = succ μ < κ by the limit property, and the finite case is power_lt_aleph0.

GCH is spelled inline and localized below κ, following the singularCardinalsHypothesis_of_gch precedent (Mathlib has no GCH identifier); the ℵ₀ ≤ μ restriction is load-bearing for the same reason as there.

theorem IsWeaklyInaccessible.isInaccessible_of_gch.{u} {κ : Cardinal.{u}}
    (hκ : IsWeaklyInaccessible κ)
    (hgch : ∀ μ : Cardinal.{u}, μ < κ → ℵ₀ ≤ μ →
      (2 : Cardinal.{u}) ^ μ = Order.succ μ) : κ.IsInaccessible

Sources

• Under GCH below κ, a weakly inaccessible κ is inaccessible.

Uses 1

Statement usesWeakly inaccessible cardinal

TheoremStrong limit cardinals are closed under exponentiation#✓fully proved

A strong limit κ is closed under cardinal exponentiation: x ^ y ≤ 2 ^ (x * y) (via cantor and power_mul), and x * y < κ by mul_lt_of_lt. No infiniteness hypothesis is needed — it is automatic by IsStrongLimit.aleph0_le.

theorem _root_.Cardinal.IsStrongLimit.power_lt.{u} {κ x y : Cardinal.{u}} (hκ : κ.IsStrongLimit)
    (hx : x < κ) (hy : y < κ) : x ^ y < κ

Sources

• Below a strong limit κ, x < κ and y < κ imply x ^ y < κ.

Used by 1

Used byWeak power below a strong limit cardinal equals the cardinal

TheoremExistence of an inaccessible with no inaccessibles below it#✓fully proved

If any inaccessible exists, some inaccessible has no inaccessibles below it: minimize over the initial ordinals of inaccessible cardinals (WellFounded.has_min), and any member of inaccessibleBelow would give a smaller one.

In particular the least inaccessible — if one exists — is neither Mahlo (see exists_isInaccessible_not_isMahlo in Mahlo.lean) nor an inaccessible fixed point (not_isInaccessibleFixedPoint_of_inaccessibleBelow_eq_empty above).

theorem exists_isInaccessible_inaccessibleBelow_eq_empty.{u}
    (h : ∃ κ : Cardinal.{u}, κ.IsInaccessible) :
    ∃ κ : Cardinal.{u}, κ.IsInaccessible ∧ inaccessibleBelow κ = ∅

Sources

• If any inaccessible cardinal exists, some inaccessible has no inaccessibles below it.

Uses 1

Statement usesSet of inaccessible cardinals below a cardinal

TheoremWeak power below a strong limit cardinal equals the cardinal#✓fully proved

For 2 ≤ x < κ with κ a strong limit, x ^< κ = κ: every smaller power is below κ (IsStrongLimit.power_lt), while every y < κ sits below 2 ^ y ≤ x ^< κ. No infiniteness hypothesis is needed — it is automatic by IsStrongLimit.aleph0_le.

theorem Cardinal.IsStrongLimit.powerlt_eq_self.{u} {κ x : Cardinal.{u}}
    (hκ : κ.IsStrongLimit) (hx2 : 2 ≤ x) (hx : x < κ) : x ^< κ = κ

Sources

• For 2 ≤ x < κ with κ a strong limit, x ^< κ = κ.

Uses 1

Proof usesStrong limit cardinals are closed under exponentiation

TheoremStrong limits are unbounded below an inaccessible cardinal#✓fully proved

Strong limits are unbounded below an inaccessible κ: above any a < κ sits ℶ_{a.ord + ω}, a strong limit by isStrongLimit_beth since a.ord + ω is a limit ordinal (isSuccLimit_add), and below κ since (a.ord + ω).card = a.ord.card + ℵ₀ < κ (add_lt_of_lt).

theorem Cardinal.IsInaccessible.exists_isStrongLimit_between.{u} {κ : Cardinal.{u}}
    (hκ : κ.IsInaccessible) {a : Cardinal.{u}} (ha : a < κ) :
    ∃ μ : Cardinal.{u}, a < μ ∧ μ < κ ∧ μ.IsStrongLimit

Sources

• Above any a < κ with κ inaccessible sits a strong limit cardinal below κ.

Uses 1

Proof usesThe beth hierarchy stays below an inaccessible cardinal

DefinitionSet of regular cardinals below a cardinal#✓fully proved

The regular cardinals below κ, carried as initial ordinals — parallel to inaccessibleBelow, and definitionally the stationary set in IsWeaklyMahlo. Spelled with Mathlib's Ordinal.IsInitial.

def regularBelow.{u} (κ : Cardinal.{u}) : Set (Set.Iio κ.ord) :=
  {α | α.val.card.IsRegular ∧ α.val.IsInitial}

Sources

• regularBelow κ is the set of initial ordinals below κ whose cardinals are regular.

TheoremA regular beth fixed point is uncountable#✓fully proved

A regular beth fixed point is uncountable: regularity gives ℵ₀ ≤ κ, and κ = ℵ₀ fails the fixed-point equation since ℶ_ω > ℶ_0 = ℵ₀.

theorem aleph0_lt_of_isRegular_beth_ord.{u} {κ : Cardinal.{u}}
    (hreg : κ.IsRegular) (hbeth : (ℶ_ κ.ord : Cardinal.{u}) = κ) : ℵ₀ < κ

Sources

• A regular beth fixed point is uncountable.

Used by 1

Used byA regular beth fixed point is inaccessible

TheoremA regular beth fixed point is inaccessible#✓fully proved

Converse to IsInaccessible.beth_ord: a regular beth fixed point is inaccessible. Uncountability is derived, not assumed (aleph0_lt_of_isRegular_beth_ord); for x < κ, 2 ^ x ≤ 2 ^ ℶ_{x.ord} = ℶ_{succ x.ord} < κ, using that κ.ord is a limit ordinal.

Regularity is genuinely needed — the first beth fixed point is singular — so this does not promote a bare fixed point.

theorem Cardinal.IsInaccessible.of_isRegular_beth_ord.{u} {κ : Cardinal.{u}}
    (hreg : κ.IsRegular) (hbeth : (ℶ_ κ.ord : Cardinal.{u}) = κ) :
    κ.IsInaccessible

Sources

• A regular beth fixed point is inaccessible.

Uses 1 · Used by 1

Proof usesA regular beth fixed point is uncountable

Used byInaccessible cardinals are the regular beth fixed points

TheoremInaccessible cardinals are the regular beth fixed points#✓fully proved

κ is inaccessible iff it is regular and a beth fixed point (uncountability is automatic by aleph0_lt_of_isRegular_beth_ord): this packages of_isRegular_beth_ord with Mathlib's IsInaccessible.beth_ord.

theorem Cardinal.isInaccessible_iff_isRegular_beth_ord.{u} {κ : Cardinal.{u}} :
    κ.IsInaccessible ↔ κ.IsRegular ∧ (ℶ_ κ.ord : Cardinal.{u}) = κ

Sources

• κ is inaccessible if and only if κ is regular and a beth fixed point.

Uses 1

Proof usesA regular beth fixed point is inaccessible

TheoremExactly \(\kappa\) inaccessibles lie below an inaccessible fixed point#✓fully proved

The fixed-point equation forces #(inaccessibleBelow κ) = lift κ (card_type): the companion to the upper bound mk_inaccessibleBelow_le.

theorem IsInaccessibleFixedPoint.mk_inaccessibleBelow.{u} {κ : Cardinal.{u}}
    (h : IsInaccessibleFixedPoint κ) :
    #↥(inaccessibleBelow κ) = Cardinal.lift.{u+1} κ

Sources

• Below an inaccessible fixed point κ there are exactly κ inaccessible cardinals.

Uses 2 · Used by 1

Statement usesInaccessible fixed point · Set of inaccessible cardinals below a cardinal

Used byInaccessibles are unbounded below an inaccessible fixed point

TheoremInaccessibles are unbounded below an inaccessible fixed point#✓fully proved

Inaccessibles below an inaccessible fixed point are unbounded: if they were bounded by a, the set would inject into Iic a.val, hence have size at most lift (a.val + 1).card < lift κ — contradicting mk_inaccessibleBelow.

theorem IsInaccessibleFixedPoint.exists_gt.{u} {κ : Cardinal.{u}}
    (h : IsInaccessibleFixedPoint κ) (a : ↥(Set.Iio κ.ord)) :
    ∃ b ∈ inaccessibleBelow κ, a.val < b.val

Sources

• Inaccessibles below an inaccessible fixed point are unbounded.

Uses 3

Statement usesInaccessible fixed point · Set of inaccessible cardinals below a cardinal

Proof usesExactly \(\kappa\) inaccessibles lie below an inaccessible fixed point

TheoremLimit cardinals are unbounded below a weakly inaccessible cardinal#✓fully proved

Limit cardinals are unbounded below a weakly inaccessible κ: the sup of the ω-chain μ 0 = succ (max a ℵ₀), μ (n+1) = succ (μ n) stays below κ (sum_lt_of_isRegular), exceeds a, and is a limit since every x < σ lies below some μ n (exists_lt_of_lt_ciSup).

theorem IsWeaklyInaccessible.exists_isSuccLimit_between.{u} {κ : Cardinal.{u}}
    (hκ : IsWeaklyInaccessible κ) {a : Cardinal.{u}} (ha : a < κ) :
    ∃ μ : Cardinal.{u}, a < μ ∧ μ < κ ∧ Order.IsSuccLimit μ

Sources

• Above any a < κ with κ weakly inaccessible sits a limit cardinal below κ.

Uses 1

Statement usesWeakly inaccessible cardinal

TheoremSupremum of a bounded set of initial ordinals is initial#✓fully proved

The sup of a bounded set of initial ordinals is initial: if σ.card.ord < σ then some member exceeds σ.card.ord, trapping it strictly between itself and its own initial ordinal.

theorem sSup_initial_of_forall_initial.{u} {T : Set Ordinal.{u}} (hbdd : BddAbove T)
    (h : ∀ t ∈ T, t.IsInitial) : (sSup T).IsInitial

Sources

• The supremum of a bounded set of initial ordinals is initial.

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.