Def MetricSpace.replaceBornology

Modification history

2024-08-17 20:49

Mathlib/Topology/MetricSpace/Defs.lean

chore: follow the "reducible non-instances" library note (#15850) …

Deleted MetricSpace.replaceBornology View on Github →

2024-08-16 01:08

Mathlib/Topology/MetricSpace/Basic.lean

chore: splitting up metric spaces files (#15790)

Modified MetricSpace.replaceBornology View on Github →

2023-03-03 17:48

Mathlib/Topology/MetricSpace/Basic.lean

feat: port Topology.MetricSpace.Basic (#2425)

Added MetricSpace.replaceBornology View on Github →