# mathlib3documentation

topology.metric_space.antilipschitz

# Antilipschitz functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

def antilipschitz_with {α : Type u_1} {β : Type u_2} (K : nnreal) (f : α β) :
Prop

We say that f : α → β is antilipschitz_with K if for any two points x, y we have edist x y ≤ K * edist (f x) (f y).

Equations
theorem antilipschitz_with.edist_lt_top {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (h : f) (x y : α) :
theorem antilipschitz_with.edist_ne_top {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (h : f) (x y : α) :
theorem antilipschitz_with_iff_le_mul_nndist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} :
(x y : α), K * has_nndist.nndist (f x) (f y)
theorem antilipschitz_with.le_mul_nndist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} :
(x y : α), K * has_nndist.nndist (f x) (f y)

Alias of the forward direction of antilipschitz_with_iff_le_mul_nndist.

theorem antilipschitz_with.of_le_mul_nndist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} :
( (x y : α), K * has_nndist.nndist (f x) (f y))

Alias of the reverse direction of antilipschitz_with_iff_le_mul_nndist.

theorem antilipschitz_with_iff_le_mul_dist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} :
(x y : α), K * has_dist.dist (f x) (f y)
theorem antilipschitz_with.le_mul_dist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} :
(x y : α), K * has_dist.dist (f x) (f y)

Alias of the forward direction of antilipschitz_with_iff_le_mul_dist.

theorem antilipschitz_with.of_le_mul_dist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} :
( (x y : α), K * has_dist.dist (f x) (f y))

Alias of the reverse direction of antilipschitz_with_iff_le_mul_dist.

theorem antilipschitz_with.mul_le_nndist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (x y : α) :
theorem antilipschitz_with.mul_le_dist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (x y : α) :
(K)⁻¹ * has_dist.dist (f x) (f y)
@[protected, nolint]
def antilipschitz_with.K {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) :

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.

Equations
• hf.K = K
@[protected]
theorem antilipschitz_with.injective {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) :
theorem antilipschitz_with.mul_le_edist {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (x y : α) :
(K)⁻¹ * has_edist.edist (f x) (f y)
theorem antilipschitz_with.ediam_preimage_le {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (s : set β) :
theorem antilipschitz_with.le_mul_ediam_image {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (s : set α) :
@[protected]
theorem antilipschitz_with.id {α : Type u_1}  :
theorem antilipschitz_with.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Kg : nnreal} {g : β γ} (hg : g) {Kf : nnreal} {f : α β} (hf : f) :
antilipschitz_with (Kf * Kg) (g f)
theorem antilipschitz_with.restrict {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (s : set α) :
(s.restrict f)
theorem antilipschitz_with.cod_restrict {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) {s : set β} (hs : (x : α), f x s) :
s hs)
theorem antilipschitz_with.to_right_inv_on' {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} {s : set α} (hf : (s.restrict f)) {g : β α} {t : set β} (g_maps : t s) (g_inv : t) :
(t.restrict g)
theorem antilipschitz_with.to_right_inv_on {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) {g : β α} {t : set β} (h : t) :
(t.restrict g)
theorem antilipschitz_with.to_right_inverse {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) {g : β α} (hg : f) :
theorem antilipschitz_with.comap_uniformity_le {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) :
@[protected]
theorem antilipschitz_with.uniform_inducing {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (hfc : uniform_continuous f) :
@[protected]
theorem antilipschitz_with.uniform_embedding {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (hfc : uniform_continuous f) :
theorem antilipschitz_with.is_complete_range {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (hfc : uniform_continuous f) :
theorem antilipschitz_with.is_closed_range {α : Type u_1} {β : Type u_2} {f : α β} {K : nnreal} (hf : f) (hfc : uniform_continuous f) :
theorem antilipschitz_with.closed_embedding {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) (hfc : uniform_continuous f) :
theorem antilipschitz_with.subtype_coe {α : Type u_1} (s : set α) :
theorem antilipschitz_with.of_subsingleton {α : Type u_1} {β : Type u_2} {f : α β} [subsingleton α] {K : nnreal} :
@[protected]
theorem antilipschitz_with.subsingleton {α : Type u_1} {β : Type u_2} {f : α β} (h : f) :

If f : α → β is 0-antilipschitz, then α is a subsingleton.

theorem antilipschitz_with.bounded_preimage {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) {s : set β} (hs : metric.bounded s) :
theorem antilipschitz_with.tendsto_cobounded {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) :
@[protected]
theorem antilipschitz_with.proper_space {β : Type u_2} {α : Type u_1} [metric_space α] {K : nnreal} {f : α β} [proper_space α] (hK : f) (f_cont : continuous f) (hf : function.surjective f) :

The image of a proper space under an expanding onto map is proper.

theorem antilipschitz_with.bounded_of_image2_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) {K₁ : nnreal} (hf : (b : β), (λ (a : α), f a b)) {s : set α} {t : set β} (hst : metric.bounded s t)) :
theorem antilipschitz_with.bounded_of_image2_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β γ} {K₂ : nnreal} (hf : (a : α), (f a)) {s : set α} {t : set β} (hst : metric.bounded s t)) :
theorem lipschitz_with.to_right_inverse {α : Type u_1} {β : Type u_2} {K : nnreal} {f : α β} (hf : f) {g : β α} (hg : f) :
@[protected]
theorem lipschitz_with.proper_space {α : Type u_1} {β : Type u_2} [metric_space β] [proper_space β] {K : nnreal} {f : α ≃ₜ β} (hK : f) :

The preimage of a proper space under a Lipschitz homeomorphism is proper.