# Commit 2020-03-03 20:14 545dd03d

View on Github →feat(topology/metric_space/antilipschitz): define `antilipschitz_with`

(#2075)

- chore(data/real/ennreal): weaker assumptions in
`sub_mul`

, add`coe_inv_le`

- feat(topology/metric_space/antilipschitz): define
`antilipschitz_with`

Also make some proofs use facts about`antilipschitz_with`

. - Rename inequalities, move
`K`

to the other side This way it's easier to glue it with the rest of the library, and we can avoid assuming`0 < K`

in many lemmas.