Prove2Me

GCH: ℵαℵβ=ℵα\aleph_\alpha^{\aleph_\beta}=\aleph_\alpha when β+1<α\beta+1<\alpha, ℵβ<cf(ℵα)\aleph_\beta<\mathrm{cf}(\aleph_\alpha)

Proved
ContinuumHypothesis.gch_aleph_pow_of_lt_cof

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

cardinal-arithmeticcofinalityset-theory

Assume GCH. For ordinals α,β\alpha,\beta with β+1<α\beta+1<\alpha and ℵβ<cf(ℵα)\aleph_\beta<\mathrm{cf}(\aleph_\alpha) (cofinality),

ℵαℵβ=ℵα.\aleph_\alpha^{\aleph_\beta}=\aleph_\alpha.
Preamble
import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u
Formal statement
namespace ContinuumHypothesis

theorem gch_aleph_pow_of_lt_cof (h : GCH.{u}) (α β : Ordinal.{u}) (hβα : β + 1 < α)
    (hcof : ℵ_ β < (ℵ_ α).ord.cof) :
    ℵ_ α ^ ℵ_ β = ℵ_ α := by sorry

end ContinuumHypothesis
Source
Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; section 'Implications of GCH for cardinal exponentiation', second bullet; Hayden–Kennison (1968), p. 147, exercise 76.
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph