Revision #1731 → #2912 · back to history
modifiedCardinality355927815661
| Field | From #1731 | To #2912 |
|---|
| note | `Cardinal.mk α` (notation `#α`) is exactly the cardinality of a type/set. | `Cardinal.mk α` (notation `#α`) is the cardinality of a type. |
modifiedFunction6959476fdc97
| Field | From #1731 | To #2912 |
|---|
| note | Functions are the primitive dependent/non-dependent arrow (`α → β`) type of Lean's type theory. | Functions are the primitive non-dependent arrow (`α → β`) type of Lean's type theory; no named Mathlib decl. |
addedVon Neumann cardinal assignment9c034c6d9d7a
addedCantor set has Lebesgue measure zero44ff61968637
addedEmpty function4375fe3f3aa8