Kőnig: $\mathrm{cf}(2^{\aleph_0})>\aleph_0$

Proved

ContinuumHypothesis.koenig_aleph0_lt_cof_two_pow_aleph0

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

cardinal-arithmeticcofinalityset-theory

The cardinality of the continuum does not have cofinality $\omega$ :

\mathrm{cf}\big(2^{\aleph_0}\big)>\aleph_0 .

So $2^{\aleph_0}$ cannot be $\aleph_\omega$ , $\aleph_{\omega_1+\omega}$ , or any cardinal of cofinality $\omega$ .

Preamble

import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u

Formal statement

namespace ContinuumHypothesis

theorem koenig_aleph0_lt_cof_two_pow_aleph0 : ℵ₀ < ((2 : Cardinal.{0}) ^ ℵ₀).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 'Independence from ZFC', paragraph 4 ('per Kőnig's theorem, it is not consistent to assume 2^ℵ₀ is ℵ_ω or ℵ_{ω₁+ω} or any cardinal with cofinality ω').

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

Kőnig: cf(2ℵ0)>ℵ0\mathrm{cf}(2^{\aleph_0})>\aleph_0cf(2ℵ0​)>ℵ0​

Kőnig: $\mathrm{cf}(2^{\aleph_0})>\aleph_0$