GCH $\iff 2^{\aleph_\alpha}=\aleph_{\alpha+1}$ for all $\alpha$

Proved

ContinuumHypothesis.gch_iff_two_pow_aleph_eq_aleph_succ

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

cardinal-arithmeticset-theory

(Cantor's aleph hypothesis.) The generalized continuum hypothesis — no infinite cardinal $\kappa$ has a cardinal strictly between $\kappa$ and $2^\kappa$ — is equivalent to

2^{\aleph_\alpha}=\aleph_{\alpha+1}\quad\text{for every ordinal }\alpha.

Preamble

import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u

Formal statement

namespace ContinuumHypothesis

theorem gch_iff_two_pow_aleph_eq_aleph_succ :
    GCH.{u} ↔ ∀ α : Ordinal.{u}, (2 : Cardinal.{u}) ^ ℵ_ α = ℵ_ (α + 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 'Generalized continuum hypothesis', paragraph 1 ('GCH is equivalent to: ℵ_{α+1} = 2^{ℵ_α} for every ordinal α').

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

GCH ⟺ 2ℵα=ℵα+1\iff 2^{\aleph_\alpha}=\aleph_{\alpha+1}⟺2ℵα​=ℵα+1​ for all α\alphaα

GCH $\iff 2^{\aleph_\alpha}=\aleph_{\alpha+1}$ for all $\alpha$