Revision #1257 → #2580 · back to history
modifiedClosed intervals in R are compactebe886d8eb69
| Field | From #1257 | To #2580 |
|---|
| mathlib.decl | isCompact_Icc | CompactIccSpace.isCompact_Icc |
| provenance | ai | ai-moderated |
modifiedHeine–Borel theorem5096e5bb9cc4
| Field | From #1257 | To #2580 |
|---|
| mathlib.decl | isCompact_iff_isClosed_bounded | Metric.isCompact_iff_isClosed_bounded |
| provenance | ai | ai-moderated |
modifiedBasis for finite productsb692df66f53b
| Field | From #1257 | To #2580 |
|---|
| mathlib.decl | IsTopologicalBasis.prod | TopologicalSpace.IsTopologicalBasis.prod |
| provenance | ai | ai-moderated |
modifiedSeparable space3a6a7327f000
| Field | From #1257 | To #2580 |
|---|
| mathlib.decl | SeparableSpace | TopologicalSpace.SeparableSpace |
| provenance | ai | ai-moderated |
modifiedSecond-countable implicationsb2f28179f939
| Field | From #1257 | To #2580 |
|---|
| mathlib.decl | SecondCountableTopology.to_firstCountableTopology | TopologicalSpace.SecondCountableTopology.to_firstCountableTopology |
| provenance | ai | ai-moderated |
modifiedMetrization theorems37f368c0b77e
| Field | From #1257 | To #2580 |
|---|
| mathlib.decl | metrizableSpace_of_t3_secondCountable | TopologicalSpace.metrizableSpace_of_t3_secondCountable |
| provenance | ai | ai-moderated |