Kőnig: $2^{\aleph_0}\neq\aleph_\alpha$ when $\mathrm{cf}(\alpha)=\omega$

Proved

ContinuumHypothesis.koenig_two_pow_aleph0_ne_aleph_of_cof_eq_aleph0

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

cardinal-arithmeticcofinalityset-theory

(Kőnig, 1906; with Hausdorff's notion of cofinality.) For every ordinal $\alpha$ of cofinality $\omega$ ,

2^{\aleph_0}\neq\aleph_\alpha.

For example $2^{\aleph_0}\neq\aleph_\omega$ .

Preamble

import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u

Formal statement

namespace ContinuumHypothesis

theorem koenig_two_pow_aleph0_ne_aleph_of_cof_eq_aleph0 (α : Ordinal.{0}) (hα : α.cof = ℵ₀) :
    (2 : Cardinal.{0}) ^ ℵ₀ ≠ ℵ_ α := by sorry

end ContinuumHypothesis

Source

Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; section 'History', paragraph 4 ('Kőnig's theorem … shows that 2^ℵ₀ cannot equal ℵ_α for α with cofinality ω. For example, 2^ℵ₀ ≠ ℵ_ω').

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: 2ℵ0≠ℵα2^{\aleph_0}\neq\aleph_\alpha2ℵ0​=ℵα​ when cf(α)=ω\mathrm{cf}(\alpha)=\omegacf(α)=ω

Kőnig: $2^{\aleph_0}\neq\aleph_\alpha$ when $\mathrm{cf}(\alpha)=\omega$