Continuum hypothesis

DefinitionContinuum hypothesis#✓fully proved

CH: 2^{ℵ₀}=ℵ₁

def ContinuumHypothesis.{u} : Prop := (2 : Cardinal.{u}) ^ ℵ₀ = ℵ₁

Used by 1

Used byEquivalent forms of the continuum hypothesis

TheoremEquivalent forms of the continuum hypothesis#✓fully proved

1. The continuum hypothesis holds if and only if the continuum equals ℵ₁. 2. The continuum hypothesis holds if and only if the continuum is at most ℵ₁. 3. The continuum hypothesis holds if and only if the reals have cardinality ℵ₁, i.e. |ℝ| = ℵ₁. 4. The continuum hypothesis holds if and only if there is no cardinal strictly between ℵ₀ and the continuum. 5.

The full informal statement is in the module documentation directly above.

theorem continuumHypothesis_iff_continuum_eq_aleph_one.{u} :
    ContinuumHypothesis.{u} ↔ (𝔠 : Cardinal.{u}) = ℵ₁

Uses 1

Statement usesContinuum hypothesis

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.