Commit 2025-02-26 19:52 9d6c1fa8
View on Github →chore (Topology/MetricSpace): remove duplicate instances (#22304) Remove some duplicate instances for type synonyms, and move some lemmas. Moves:
- instMetricSpaceAddOpposite -> AddOpposite.instMetricSpace Deletions:
- instMetricSpaceMulOpposite
- instPseudoMetricSpaceOrderDual_1
- instMetricSpaceAdditive_1
- instMetricSpaceMultiplicative_1
- instMetricSpaceOrderDual_1