mathlib

97f079b7 - chore(topology/metric_space/anti_lipschitz): fix typo (#18263)

chore(topology/metric_space/anti_lipschitz): fix typo (#18263) Fix a typo in the definition of `antilipschitz_with`. I presume that the definition is correct, and was not intended as described in the docstring.