Revision #2420 → #2664 · back to history
modifiedNeighbourhood system on the real line2320de620fc2
| Field | From #2420 | To #2664 |
|---|
| mathlib.decl | Real.instTopologicalSpace | Real.pseudoMetricSpace |
| provenance | ai | ai-moderated |
modifiedLattice of topologies on a set0e9a0f525388
| Field | From #2420 | To #2664 |
|---|
| mathlib.decl | TopologicalSpace.instCompleteLatticeTopologicalSpace | TopologicalSpace.instCompleteLattice |
| provenance | ai | ai-moderated |
modifiedStandard topology on the real line3b8fdc3c6abe
| Field | From #2420 | To #2664 |
|---|
| mathlib.decl | Real.instTopologicalSpace | Real.pseudoMetricSpace |
| provenance | ai | ai-moderated |
modifiedTopology from a filtera43e0796b2d1
| Field | From #2420 | To #2664 |
|---|
| mathlib.decl | Filter.instTopologicalSpaceFilter | Filter.instTopologicalSpace |
| provenance | ai | ai-moderated |