Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-06 09:17 14d34b71

View on Github →

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.

Estimated changes

added theorem continuous_of_add
added theorem continuous_of_dual
added theorem continuous_of_mul
added theorem continuous_to_add
added theorem continuous_to_dual
added theorem continuous_to_mul
added theorem is_closed_map_of_add
added theorem is_closed_map_of_dual
added theorem is_closed_map_of_mul
added theorem is_closed_map_to_add
added theorem is_closed_map_to_dual
added theorem is_closed_map_to_mul
added theorem is_open_map_of_add
added theorem is_open_map_of_dual
added theorem is_open_map_of_mul
added theorem is_open_map_to_add
added theorem is_open_map_to_dual
added theorem is_open_map_to_mul
added theorem nhds_of_add
added theorem nhds_of_dual
added theorem nhds_of_mul
added theorem nhds_to_add
added theorem nhds_to_dual
added theorem nhds_to_mul
added theorem dist_of_add
added theorem dist_of_dual
added theorem dist_of_mul
added theorem dist_to_add
added theorem dist_to_dual
added theorem dist_to_mul
added theorem nndist_of_add
added theorem nndist_of_dual
added theorem nndist_of_mul
added theorem nndist_to_add
added theorem nndist_to_dual
added theorem nndist_to_mul
added theorem edist_of_add
added theorem edist_of_dual
added theorem edist_of_mul
added theorem edist_to_add
added theorem edist_to_dual
added theorem edist_to_mul
added theorem uniformity_additive