We say that a map
f : α → β between two (extended) metric spaces is
K ≥ 0, if for all
x, y we have
edist x y ≤ K * edist (f x) (f y).
For a metric space, the latter inequality is equivalent to
dist x y ≤ K * dist (f x) (f y).
K has type
ℝ≥0. This way we avoid conjuction in the definition and have
coercions both to
ennreal. We do not require
0 < K in the definition, mostly because
we do not have a
We say that
f : α → β is
antilipschitz_with K if for any two points
y we have
K * edist x y ≤ edist (f x) (f y).
Extract the constant from
hf : antilipschitz_with K f. This is useful, e.g.,
K is given by a long formula, and we want to reuse this value.