CH $\iff 2^{\aleph_0}=\aleph_1$

Proved

ContinuumHypothesis.ch_iff_two_pow_aleph0_eq_aleph1

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

cardinal-arithmeticset-theory

Assuming the axiom of choice (as Lean does), the continuum hypothesis — no $S\subseteq\mathbb R$ has $\aleph_0<|S|<2^{\aleph_0}$ — is equivalent to

2^{\aleph_0}=\aleph_1,

where $\aleph_1$ is the least cardinal greater than $\aleph_0$ .

Preamble

import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u

Formal statement

namespace ContinuumHypothesis

theorem ch_iff_two_pow_aleph0_eq_aleph1 : CH ↔ (2 : Cardinal.{0}) ^ ℵ₀ = ℵ_ 1 := by sorry

end ContinuumHypothesis

Source

Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; end of section 'Cardinality of infinite sets' ('Assuming the axiom of choice, there is a unique smallest cardinal number ℵ₁ greater than ℵ₀, and the continuum hypothesis is in turn equivalent to the equality 2^ℵ₀ = ℵ₁') and introduction.

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

CH ⟺ 2ℵ0=ℵ1\iff 2^{\aleph_0}=\aleph_1⟺2ℵ0​=ℵ1​

CH $\iff 2^{\aleph_0}=\aleph_1$