mathlib

14d34b71 - feat(topology/metric_space/*): `additive`/`multiplicative`/`order_dual` instances (#15704)

feat(topology/metric_space/*): `additive`/`multiplicative`/`order_dual` instances (#15704) Transfer topology, bornology, uniform space and metric space instances to `additive`, `multiplicative` and `order_dual`.