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

Estimated changes

deleted theorem nndist_ofAdd
deleted theorem nndist_ofDual
deleted theorem nndist_ofMul
deleted theorem nndist_toAdd
deleted theorem nndist_toDual
deleted theorem nndist_toMul
added theorem nndist_ofAdd
added theorem nndist_ofDual
added theorem nndist_ofMul
added theorem nndist_toAdd
added theorem nndist_toDual
added theorem nndist_toMul