Commit 2021-03-25 19:35 e0547059
View on Github →refactor(topology/metric_space/antilipschitz): generalize to pseudo_metric_space (#6841)
This is part of a series of PR to introduce semi_normed_group in mathlib.
We introduce here anti Lipschitz maps for pseudo_emetric_space
.