GCH implies SCH

Proved

SingularCardinals.sch_of_gch

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

cardinal-arithmeticset-theory

If the generalized continuum hypothesis holds, that is $2^\lambda=\lambda^+$ for every infinite cardinal $\lambda$ , then the singular cardinals hypothesis holds: for every singular strong limit cardinal $\kappa$ ,

2^\kappa=\kappa^+.

Together with the consistency of GCH this is the source's argument that SCH is consistent with ZFC.

Preamble

import Mathlib
import Definitions.Def_JechStationary
import Definitions.Def_SingularCardinals_basic

universe u

open Cardinal

Formal statement

namespace SingularCardinals

theorem sch_of_gch (h : GCH.{u}) : SCH.{u} := by sorry

end SingularCardinals

Source

Wikipedia, "Singular cardinals hypothesis", revision oldid=1349753131, https://en.wikipedia.org/w/index.php?title=Singular_cardinals_hypothesis&oldid=1349753131, second paragraph ("Since SCH is a consequence of GCH ...") and last paragraph ("As was noted above, GCH implies SCH").

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph