Revision #1117 → #2730 · back to history
modifiedKőnig's theorem43463be61c9a
| Field | From #1117 | To #2730 |
|---|
| note | Cardinal.sum_lt_prod is explicitly labelled König's theorem (∀i, f i < g i → sum f < prod g). | Cardinal.sum_lt_prod is König's theorem: (∀ i, f i < g i) → sum f < prod g. |
modifiedRationals are countablec6bfb88ff425
| Field | From #1117 | To #2730 |
|---|
| mathlib.module | Mathlib.Data.Rat.Cardinal | Mathlib.SetTheory.Cardinal.Rat |
| note | Cardinal.mkRat proves #ℚ = ℵ₀ = #ℤ (Cardinal.mk_int), giving the bijection with the integers. | Cardinal.mkRat proves #ℚ = ℵ₀, matching Cardinal.mk_int and giving the bijection with the integers. |
modifiedIntegers strictly smaller than reals716dde66202e
| Field | From #1117 | To #2730 |
|---|
| note | Cardinal.aleph0_lt_continuum (ℵ₀ < 𝔠) with Cardinal.mk_int (#ℤ=ℵ₀) and Cardinal.mk_real (#ℝ=𝔠) gives #ℤ < #ℝ. | Cardinal.aleph0_lt_continuum (ℵ₀ < 𝔠) with Cardinal.mk_int (#ℤ = ℵ₀) and Cardinal.mk_real (#ℝ = 𝔠) yields #ℤ < #ℝ. |
addedReals equinumerous with powerset of integersa1ce01626dbc