Def uniformSpaceOfEDist

Modification history

2026-03-24 02:02
Mathlib/Topology/EMetricSpace/Defs.lean
chore: bump toolchain to `v4.29.0-rc7` (#37034) …
Deleted uniformSpaceOfEDistView on Github →
2025-07-01 09:03
Mathlib/Topology/EMetricSpace/Defs.lean
feat: constructor for emetric space with a preexisting topology (#26503) …
Modified uniformSpaceOfEDistView on Github →
2024-08-16 01:08
Mathlib/Topology/EMetricSpace/Basic.lean
chore: splitting up metric spaces files (#15790)
Modified uniformSpaceOfEDistView on Github →
2023-03-03 08:09
Mathlib/Topology/MetricSpace/EMetricSpace.lean
feat: port Topology.MetricSpace.EMetricSpace (#2407)
Added uniformSpaceOfEDistView on Github →