mathlib documentation

topology.metric_space.antilipschitz

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 nnreal. This way we avoid conjuction in the definition and have coercions both to and ennreal. 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} [emetric_space α] [emetric_space β] :
ℝ≥0(α → β) → Prop

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
theorem antilipschitz_with_iff_le_mul_dist {α : Type u_1} {β : Type u_2} [metric_space α] [metric_space β] {K : ℝ≥0} {f : α → β} :
antilipschitz_with K f ∀ (x y : α), dist x y (K) * dist (f x) (f y)

theorem antilipschitz_with.mul_le_dist {α : Type u_1} {β : Type u_2} [metric_space α] [metric_space β] {K : ℝ≥0} {f : α → β} (hf : antilipschitz_with K f) (x y : α) :
(K⁻¹) * dist x y dist (f x) (f y)

@[nolint]
def antilipschitz_with.K {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {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
theorem antilipschitz_with.injective {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} :

theorem antilipschitz_with.mul_le_edist {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : antilipschitz_with K f) (x y : α) :
(K⁻¹) * edist x y edist (f x) (f y)

theorem antilipschitz_with.id {α : Type u_1} [emetric_space α] :

theorem antilipschitz_with.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [emetric_space α] [emetric_space β] [emetric_space γ] {Kg : ℝ≥0} {g : β → γ} (hg : antilipschitz_with Kg g) {Kf : ℝ≥0} {f : α → β} :

theorem antilipschitz_with.restrict {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : antilipschitz_with K f) (s : set α) :

theorem antilipschitz_with.cod_restrict {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : antilipschitz_with K f) {s : set β} (hs : ∀ (x : α), f x s) :

theorem antilipschitz_with.to_right_inv_on' {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} {s : set α} (hf : antilipschitz_with K (set.restrict f s)) {g : β → α} {t : set β} :

theorem antilipschitz_with.to_right_inv_on {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : antilipschitz_with K f) {g : β → α} {t : set β} :

theorem antilipschitz_with.to_right_inverse {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : antilipschitz_with K f) {g : β → α} :

theorem antilipschitz_with.uniform_embedding {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} :

theorem antilipschitz_with.subtype_coe {α : Type u_1} [emetric_space α] (s : set α) :

theorem antilipschitz_with.of_subsingleton {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {f : α → β} [subsingleton α] {K : ℝ≥0} :

theorem lipschitz_with.to_right_inverse {α : Type u_1} {β : Type u_2} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K f) {g : β → α} :