Antilipschitz functions #
We say that a map f : α → β
between two (extended) metric spaces is
antilipschitz_with K
, 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)
.
Implementation notes #
The parameter K
has type ℝ≥0
. This way we avoid conjuction in the definition and have
coercions both to ℝ
and ℝ≥0∞
. We do not require 0 < K
in the definition, mostly because
we do not have a posreal
type.
We say that f : α → β
is antilipschitz_with K
if for any two points x
, y
we have
K * edist x y ≤ edist (f x) (f y)
.
Equations
- antilipschitz_with K f = ∀ (x y : α), has_edist.edist x y ≤ ↑K * has_edist.edist (f x) (f y)
Alias of the forward direction of antilipschitz_with_iff_le_mul_nndist
.
Alias of the reverse direction of antilipschitz_with_iff_le_mul_nndist
.
Alias of the forward direction of antilipschitz_with_iff_le_mul_dist
.
Alias of the reverse direction of antilipschitz_with_iff_le_mul_dist
.
Extract the constant from hf : antilipschitz_with K f
. This is useful, e.g.,
if K
is given by a long formula, and we want to reuse this value.
If f : α → β
is 0
-antilipschitz, then α
is a subsingleton
.
The image of a proper space under an expanding onto map is proper.