# Documentation

Mathlib.Topology.MetricSpace.Antilipschitz

# Antilipschitz functions #

We say that a map f : α → β between two (extended) metric spaces is AntilipschitzWith 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 conjunction 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 AntilipschitzWith {α : Type u_1} {β : Type u_2} (K : NNReal) (f : αβ) :

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

Instances For
theorem AntilipschitzWith.edist_lt_top {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (h : ) (x : α) (y : α) :
edist x y <
theorem AntilipschitzWith.edist_ne_top {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (h : ) (x : α) (y : α) :
theorem antilipschitzWith_iff_le_mul_nndist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} :
∀ (x y : α), nndist x y K * nndist (f x) (f y)
theorem AntilipschitzWith.le_mul_nndist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} :
∀ (x y : α), nndist x y K * nndist (f x) (f y)

Alias of the forward direction of antilipschitzWith_iff_le_mul_nndist.

theorem AntilipschitzWith.of_le_mul_nndist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} :
(∀ (x y : α), nndist x y K * nndist (f x) (f y)) →

Alias of the reverse direction of antilipschitzWith_iff_le_mul_nndist.

theorem antilipschitzWith_iff_le_mul_dist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} :
∀ (x y : α), dist x y K * dist (f x) (f y)
theorem AntilipschitzWith.le_mul_dist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} :
∀ (x y : α), dist x y K * dist (f x) (f y)

Alias of the forward direction of antilipschitzWith_iff_le_mul_dist.

theorem AntilipschitzWith.of_le_mul_dist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} :
(∀ (x y : α), dist x y K * dist (f x) (f y)) →

Alias of the reverse direction of antilipschitzWith_iff_le_mul_dist.

theorem AntilipschitzWith.mul_le_nndist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) (x : α) (y : α) :
K⁻¹ * nndist x y nndist (f x) (f y)
theorem AntilipschitzWith.mul_le_dist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) (x : α) (y : α) :
K⁻¹ * dist x y dist (f x) (f y)
def AntilipschitzWith.k {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (_hf : ) :

Extract the constant from hf : AntilipschitzWith K f. This is useful, e.g., if K is given by a long formula, and we want to reuse this value.

Instances For
theorem AntilipschitzWith.injective {α : Type u_4} {β : Type u_5} [] {K : NNReal} {f : αβ} (hf : ) :
theorem AntilipschitzWith.mul_le_edist {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) (x : α) (y : α) :
(K)⁻¹ * edist x y edist (f x) (f y)
theorem AntilipschitzWith.ediam_preimage_le {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) (s : Set β) :
EMetric.diam (f ⁻¹' s) K *
theorem AntilipschitzWith.le_mul_ediam_image {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) (s : Set α) :
K * EMetric.diam (f '' s)
theorem AntilipschitzWith.id {α : Type u_1} :
theorem AntilipschitzWith.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Kg : NNReal} {g : βγ} (hg : ) {Kf : NNReal} {f : αβ} (hf : ) :
AntilipschitzWith (Kf * Kg) (g f)
theorem AntilipschitzWith.restrict {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) (s : Set α) :
theorem AntilipschitzWith.codRestrict {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) {s : Set β} (hs : ∀ (x : α), f x s) :
theorem AntilipschitzWith.to_rightInvOn' {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} {s : Set α} (hf : ) {g : βα} {t : Set β} (g_maps : Set.MapsTo g t s) (g_inv : ) :
theorem AntilipschitzWith.to_rightInvOn {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) {g : βα} {t : Set β} (h : ) :
theorem AntilipschitzWith.to_rightInverse {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) {g : βα} (hg : ) :
theorem AntilipschitzWith.comap_uniformity_le {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) :
theorem AntilipschitzWith.uniformInducing {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) (hfc : ) :
theorem AntilipschitzWith.uniformEmbedding {α : Type u_4} {β : Type u_5} [] {K : NNReal} {f : αβ} (hf : ) (hfc : ) :
theorem AntilipschitzWith.isComplete_range {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} [] (hf : ) (hfc : ) :
theorem AntilipschitzWith.isClosed_range {α : Type u_4} {β : Type u_5} [] [] {f : αβ} {K : NNReal} (hf : ) (hfc : ) :
theorem AntilipschitzWith.closedEmbedding {α : Type u_4} {β : Type u_5} [] [] {K : NNReal} {f : αβ} [] (hf : ) (hfc : ) :
theorem AntilipschitzWith.subtype_coe {α : Type u_1} (s : Set α) :
AntilipschitzWith 1 Subtype.val
theorem AntilipschitzWith.of_subsingleton {α : Type u_1} {β : Type u_2} {f : αβ} [] {K : NNReal} :
theorem AntilipschitzWith.subsingleton {α : Type u_4} {β : Type u_5} [] {f : αβ} (h : ) :

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

theorem AntilipschitzWith.isBounded_preimage {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) {s : Set β} (hs : ) :
theorem AntilipschitzWith.tendsto_cobounded {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) :
theorem AntilipschitzWith.properSpace {β : Type u_2} {α : Type u_4} [] {K : NNReal} {f : αβ} [] (hK : ) (f_cont : ) (hf : ) :

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

theorem LipschitzWith.to_rightInverse {α : Type u_1} {β : Type u_2} {K : NNReal} {f : αβ} (hf : ) {g : βα} (hg : ) :
theorem LipschitzWith.properSpace {α : Type u_1} {β : Type u_2} [] [] {K : NNReal} {f : α ≃ₜ β} (hK : ) :

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