Prove2Me

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

Proved
ContinuumHypothesis.gch_aleph_pow_of_cof_le

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\ge\mathrm{cf}(\aleph_\alpha),

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

theorem gch_aleph_pow_of_cof_le (h : GCH.{u}) (α β : Ordinal.{u}) (hβα : β + 1 < α)
    (hcof : (ℵ_ α).ord.cof ≤ ℵ_ β) :
    ℵ_ α ^ ℵ_ β = ℵ_ (α + 1) := 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', third 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