Prove2Me

GCH: ℵαℵβ=ℵβ+1\aleph_\alpha^{\aleph_\beta}=\aleph_{\beta+1} when α≤β+1\alpha\le\beta+1

Proved
ContinuumHypothesis.gch_aleph_pow_of_le_succ

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

cardinal-arithmeticset-theory

Assume GCH. For ordinals α,β\alpha,\beta with α≤β+1\alpha\le\beta+1,

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

theorem gch_aleph_pow_of_le_succ (h : GCH.{u}) (α β : Ordinal.{u}) (hαβ : α ≤ β + 1) :
    ℵ_ α ^ ℵ_ β = ℵ_ (β + 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', first bullet; Hayden–Kennison, Zermelo-Fraenkel Set Theory (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