Revision #1286 → #2585 · back to history
modifiedReal numbers are Hausdorff331f13110a31
| Field | From #1286 | To #2585 |
|---|
| mathlib.decl | t2Space_of_metrizableSpace | TopologicalSpace.t2Space_of_metrizableSpace |
| provenance | ai | ai-moderated |
modifiedMetric spaces are Hausdorffe0423f5b1bc0
| Field | From #1286 | To #2585 |
|---|
| mathlib.decl | t2Space_of_metrizableSpace | TopologicalSpace.t2Space_of_metrizableSpace |
| provenance | ai | ai-moderated |
modifiedT1 but not Hausdorff: cofinite/cocountablebfe042699a10
| Field | From #1286 | To #2585 |
|---|
| mathlib.decl | CofiniteTopology.instT1Space | instT1SpaceCofiniteTopology |
| provenance | ai | ai-moderated |
modifiedPseudometric spaces are preregular not Hausdorff1a89b4d03f98
| Field | From #1286 | To #2585 |
|---|
| mathlib.decl | PseudoMetrizableSpace.regularSpace | TopologicalSpace.PseudoMetrizableSpace.regularSpace |
| provenance | ai | ai-moderated |
modifiedPreregular spaces are R0efffbe5cebc6
| Field | From #1286 | To #2585 |
|---|
| mathlib.decl | R1Space.instR0Space | instR0Space |
| provenance | ai | ai-moderated |