Revision #1057 → #1731 · back to history
addedIdentity function (witness of reflexivity)e9b2e6432367
addedInverse of a bijection (witness of symmetry)01cc7718a6e8
addedComposition of bijections (witness of transitivity)420a1da11367
modifiedSchröder–Bernstein theorem6a73bcb89fa1
| Field | From #1057 | To #1731 |
|---|
| mathlib.decl | schroeder_bernstein | Function.Embedding.schroeder_bernstein |
| note | `schroeder_bernstein` gives a bijection from mutual injections, matching the theorem. | `Function.Embedding.schroeder_bernstein` gives a bijection from mutual injections, matching the theorem. |
modifiedRational numbers are countableea3b56984adf
| Field | From #1057 | To #1731 |
|---|
| mathlib.module | Mathlib.Data.Rat.Cardinal | Mathlib.SetTheory.Cardinal.Rat |
addedBurali-Forti paradox (ordinals form a proper class)719bba59299b
modifiedExamples of proper classes160f13c213b5
| Field | From #1057 | To #1731 |
|---|
| note | The universal class `Class.univ` exists, and `not_small_cardinal`/non-smallness of `Ordinal` express that cardinals and ordinals form proper classes. | The universal class `Class.univ` exists, and `not_small_cardinal`/`not_small_ordinal` express that cardinals and ordinals form proper classes. |