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.

Estimated changes

Modified src/topology/metric_space/antilipschitz.lean

modified theorem antilipschitz_with.closed_embedding

modified theorem antilipschitz_with.mul_le_dist

modified theorem antilipschitz_with.uniform_embedding

added theorem antilipschitz_with.uniform_embedding_of_injective

modified def antilipschitz_with

modified theorem antilipschitz_with_iff_le_mul_dist

modified theorem lipschitz_with.to_right_inverse