GCH $\Rightarrow$ ( $A<B\Rightarrow 2^A<2^B$ ) for infinite $A$

Proved

ContinuumHypothesis.gch_two_pow_strictMono

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

cardinal-arithmeticset-theory

Assume the generalized continuum hypothesis. Then for all cardinals $A,B$ with $A$ infinite,

A<B\ \Longrightarrow\ 2^A<2^B .

(Without GCH only $2^A\le 2^B$ follows; the strict form always holds for finite cardinals.)

Preamble

import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u

Formal statement

namespace ContinuumHypothesis

theorem gch_two_pow_strictMono (h : GCH.{u}) (A B : Cardinal.{u}) (hA : ℵ₀ ≤ A) (hAB : A < B) :
    (2 : Cardinal.{u}) ^ A < 2 ^ B := 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 5 ('GCH implies that this strict, stronger inequality holds for infinite cardinals as well as finite cardinals').

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 ⇒\Rightarrow⇒ (A<B⇒2A<2BA<B\Rightarrow 2^A<2^BA<B⇒2A<2B) for infinite AAA

GCH $\Rightarrow$ ( $A<B\Rightarrow 2^A<2^B$ ) for infinite $A$