Revision #2730 → #3190 · back to history
modifiedContinuum hypothesis7adf578324da
| Field | From #2730 | To #3190 |
|---|
| note | Mathlib has the provable direction ℵ₁ ≤ 𝔠 but never defines or asserts CH itself (which is independent of ZFC). | Mathlib has the provable direction ℵ₁ ≤ 𝔠 (Cardinal.aleph_one_le_continuum) but never defines or asserts CH itself, which is independent of ZFC. |
modifiedCH equivalent in aleph/beth numbersd5feb75e7a72
| Field | From #2730 | To #3190 |
|---|
| mathlib.decl | Cardinal.aleph_one_le_continuum | Cardinal.two_power_aleph0 |
| note | Mathlib has 𝔠 = 2^ℵ₀ (Cardinal.two_power_aleph0) and ℵ₁ ≤ 𝔠 but not the equation 2^ℵ₀ = ℵ₁. | Mathlib proves 𝔠 = 2^ℵ₀ (Cardinal.two_power_aleph0) and ℵ₁ ≤ 𝔠, but the equation 2^ℵ₀ = ℵ₁ is not stated. |
addedCofinality3ba7e743e97c
addedCantor's theorem (diagonal argument)61d1b5a925fe
addedConstructible universe L1b476d0d69d2
addedHartogs numberd710be6823d8