Revision #3190 → #3704 · back to history
modifiedContinuum hypothesis7adf578324da
| Field | From #3190 | To #3704 |
|---|
| kind | definition | proposition |
| provenance | ai | ai-moderated |
modifiedGeneralized continuum hypothesis7a68c80adc11
| Field | From #3190 | To #3704 |
|---|
| note | No GCH definition exists anywhere in Mathlib. | No GCH definition exists anywhere in Mathlib (loogle finds no matching decl). |
addedBijection97b4a9b50e36
addedCountable seteedc67277768
addedAxiom of choice68fd67f2c3ad
modifiedUnique smallest cardinal greater than aleph-null7981f711c720
| Field | From #3190 | To #3704 |
|---|
| note | ℵ₁ = succ ℵ₀ (Cardinal.succ_aleph0) and Cardinal.aleph_one_le_iff (ℵ₁ ≤ c ↔ ℵ₀ < c) express that ℵ₁ is the least cardinal exceeding ℵ₀. | Cardinal.aleph_one_le_iff (ℵ₁ ≤ c ↔ ℵ₀ < c), together with Cardinal.succ_aleph0, expresses that ℵ₁ is the least cardinal exceeding ℵ₀. |
addedAleph numbers7fb49c1b376a
modifiedConstructible universe L1b476d0d69d2
| Field | From #3190 | To #3704 |
|---|
| note | Gödel's constructible universe L is not developed in Mathlib. | Gödel's constructible universe L is not developed in Mathlib (only topological 'constructible' notions exist). |
modifiedFreiling's axiom of symmetry equivalent to ¬CH001b7a6cce21
| Field | From #3190 | To #3704 |
|---|
| note | Freiling's axiom of symmetry and its equivalence with ¬CH are absent from Mathlib. | Freiling's axiom of symmetry and its equivalence with ¬CH are absent from Mathlib (loogle 'Freiling' returns nothing). |
modifiedHartogs numberd710be6823d8
| Field | From #3190 | To #3704 |
|---|
| note | No Hartogs number declaration exists in Mathlib (searched for 'hartogs' and 'Ordinal.hartogs' with no match). | No Hartogs number declaration exists in Mathlib (loogle 'hartogs' returns zero matches). |