doc-next-gen

Mathlib.Topology.MetricSpace.Antilipschitz

Module docstring

{"# 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. "}

AntilipschitzWith definition
[PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : ℝ≥0) (f : α → β)
Full source 
/-- 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)`. -/
def AntilipschitzWith [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : ℝ≥0) (f : α → β) :=
  ∀ x y, edist x y ≤ K * edist (f x) (f y)
Antilipschitz function with constant $K$
Informal description
A function $f \colon \alpha \to \beta$ between two extended pseudo-metric spaces is called *antilipschitz with constant $K \geq 0$* if for all $x, y \in \alpha$, the extended distance satisfies $\text{edist}(x, y) \leq K \cdot \text{edist}(f(x), f(y))$.
AntilipschitzWith.edist_lt_top theorem
[PseudoEMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0} {f : α → β} (h : AntilipschitzWith K f) (x y : α) : edist x y < ⊤
Full source 
protected lemma AntilipschitzWith.edist_lt_top [PseudoEMetricSpace α] [PseudoMetricSpace β]
    {K : ℝ≥0} {f : α → β} (h : AntilipschitzWith K f) (x y : α) : edist x y < ⊤ :=
  (h x y).trans_lt <| ENNReal.mul_lt_top ENNReal.coe_lt_top (edist_lt_top _ _)
Finite Extended Distance Property of Antilipschitz Functions
Informal description
Let $\alpha$ be an extended pseudo-metric space and $\beta$ a pseudo-metric space. Given an antilipschitz function $f \colon \alpha \to \beta$ with constant $K \geq 0$, the extended distance between any two points $x, y \in \alpha$ is finite, i.e., $\text{edist}(x, y) < \infty$.
AntilipschitzWith.edist_ne_top theorem
[PseudoEMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0} {f : α → β} (h : AntilipschitzWith K f) (x y : α) : edist x y ≠ ⊤
Full source 
theorem AntilipschitzWith.edist_ne_top [PseudoEMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0}
    {f : α → β} (h : AntilipschitzWith K f) (x y : α) : edistedist x y ≠ ⊤ :=
  (h.edist_lt_top x y).ne
Finite Extended Distance Property of Antilipschitz Functions
Informal description
Let $\alpha$ be an extended pseudo-metric space and $\beta$ a pseudo-metric space. Given an antilipschitz function $f \colon \alpha \to \beta$ with constant $K \geq 0$, the extended distance between any two points $x, y \in \alpha$ is not infinite, i.e., $\text{edist}(x, y) \neq \infty$.
antilipschitzWith_iff_le_mul_nndist theorem
: AntilipschitzWith K f ↔ ∀ x y, nndist x y ≤ K * nndist (f x) (f y)
Full source 
theorem antilipschitzWith_iff_le_mul_nndist :
    AntilipschitzWithAntilipschitzWith K f ↔ ∀ x y, nndist x y ≤ K * nndist (f x) (f y) := by
  simp only [AntilipschitzWith, edist_nndist]
  norm_cast
Characterization of Antilipschitz Functions via Non-negative Distance: $\text{nndist}(x, y) \leq K \cdot \text{nndist}(f(x), f(y))$
Informal description
A function $f \colon \alpha \to \beta$ between two pseudometric spaces is antilipschitz with constant $K \geq 0$ if and only if for all $x, y \in \alpha$, the non-negative distance satisfies $\text{nndist}(x, y) \leq K \cdot \text{nndist}(f(x), f(y))$.
antilipschitzWith_iff_le_mul_dist theorem
: AntilipschitzWith K f ↔ ∀ x y, dist x y ≤ K * dist (f x) (f y)
Full source 
theorem antilipschitzWith_iff_le_mul_dist :
    AntilipschitzWithAntilipschitzWith K f ↔ ∀ x y, dist x y ≤ K * dist (f x) (f y) := by
  simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]
  norm_cast
Characterization of Antilipschitz Functions via Distance Inequality
Informal description
A function $f \colon \alpha \to \beta$ between pseudometric spaces is antilipschitz with constant $K \geq 0$ if and only if for all $x, y \in \alpha$, the distance satisfies $\text{dist}(x, y) \leq K \cdot \text{dist}(f(x), f(y))$.
AntilipschitzWith.mul_le_nndist theorem
(hf : AntilipschitzWith K f) (x y : α) : K⁻¹ * nndist x y ≤ nndist (f x) (f y)
Full source 
theorem mul_le_nndist (hf : AntilipschitzWith K f) (x y : α) :
    K⁻¹ * nndist x y ≤ nndist (f x) (f y) := by
  simpa only [div_eq_inv_mul] using NNReal.div_le_of_le_mul' (hf.le_mul_nndist x y)
Lower Bound on Non-negative Distance under Antilipschitz Maps: $K^{-1} \cdot \text{nndist}(x, y) \leq \text{nndist}(f(x), f(y))$
Informal description
Let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$ between two pseudometric spaces. Then for any $x, y \in \alpha$, the non-negative distance satisfies $K^{-1} \cdot \text{nndist}(x, y) \leq \text{nndist}(f(x), f(y))$.
AntilipschitzWith.mul_le_dist theorem
(hf : AntilipschitzWith K f) (x y : α) : (K⁻¹ * dist x y : ℝ) ≤ dist (f x) (f y)
Full source 
theorem mul_le_dist (hf : AntilipschitzWith K f) (x y : α) :
    (K⁻¹ * dist x y : ℝ) ≤ dist (f x) (f y) := mod_cast hf.mul_le_nndist x y
Lower Bound on Distance under Antilipschitz Maps: $K^{-1} \cdot \text{dist}(x, y) \leq \text{dist}(f(x), f(y))$
Informal description
Let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$ between two pseudometric spaces. Then for any $x, y \in \alpha$, the distance satisfies $K^{-1} \cdot \text{dist}(x, y) \leq \text{dist}(f(x), f(y))$.
AntilipschitzWith.k definition
(_hf : AntilipschitzWith K f) : ℝ≥0
Full source 
/-- 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. -/
@[nolint unusedArguments]
protected def k (_hf : AntilipschitzWith K f) : ℝ≥0 := K
Antilipschitz constant \( K \) of a function \( f \)
Informal description
Given a function \( f \colon \alpha \to \beta \) that is antilipschitz with constant \( K \), this function extracts the constant \( K \) from the proof term \( hf \). This is particularly useful when \( K \) is defined by a complex expression and needs to be reused.
AntilipschitzWith.injective theorem
{α : Type*} {β : Type*} [EMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0} {f : α → β} (hf : AntilipschitzWith K f) : Function.Injective f
Full source 
protected theorem injective {α : Type*} {β : Type*} [EMetricSpace α] [PseudoEMetricSpace β]
    {K : ℝ≥0} {f : α → β} (hf : AntilipschitzWith K f) : Function.Injective f := fun x y h => by
  simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y
Injectivity of Antilipschitz Functions
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$. Then $f$ is injective, i.e., for any $x, y \in \alpha$, if $f(x) = f(y)$, then $x = y$.
AntilipschitzWith.mul_le_edist theorem
(hf : AntilipschitzWith K f) (x y : α) : (K : ℝ≥0∞)⁻¹ * edist x y ≤ edist (f x) (f y)
Full source 
theorem mul_le_edist (hf : AntilipschitzWith K f) (x y : α) :
    (K : ℝ≥0∞)⁻¹ * edist x y ≤ edist (f x) (f y) := by
  rw [mul_comm, ← div_eq_mul_inv]
  exact ENNReal.div_le_of_le_mul' (hf x y)
Lower Bound on Image Distance for Antilipschitz Functions: $\frac{1}{K} \text{edist}(x,y) \leq \text{edist}(f(x),f(y))$
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$. Then for any $x, y \in \alpha$, the extended distance between $f(x)$ and $f(y)$ satisfies the inequality: \[ \frac{1}{K} \cdot \text{edist}(x, y) \leq \text{edist}(f(x), f(y)). \]
AntilipschitzWith.ediam_preimage_le theorem
(hf : AntilipschitzWith K f) (s : Set β) : diam (f ⁻¹' s) ≤ K * diam s
Full source 
theorem ediam_preimage_le (hf : AntilipschitzWith K f) (s : Set β) : diam (f ⁻¹' s) ≤ K * diam s :=
  diam_le fun x hx y hy => (hf x y).trans <|
    mul_le_mul_left' (edist_le_diam_of_mem (mem_preimage.1 hx) hy) K
Diameter Bound for Preimage under Antilipschitz Map: $\text{diam}(f^{-1}(s)) \leq K \cdot \text{diam}(s)$
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$. For any subset $s \subseteq \beta$, the diameter of the preimage $f^{-1}(s)$ satisfies $\text{diam}(f^{-1}(s)) \leq K \cdot \text{diam}(s)$.
AntilipschitzWith.le_mul_ediam_image theorem
(hf : AntilipschitzWith K f) (s : Set α) : diam s ≤ K * diam (f '' s)
Full source 
theorem le_mul_ediam_image (hf : AntilipschitzWith K f) (s : Set α) : diam s ≤ K * diam (f '' s) :=
  (diam_mono (subset_preimage_image _ _)).trans (hf.ediam_preimage_le (f '' s))
Diameter Bound for Image under Antilipschitz Map: $\text{diam}(s) \leq K \cdot \text{diam}(f(s))$
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$. For any subset $s \subseteq \alpha$, the diameter of $s$ satisfies $\text{diam}(s) \leq K \cdot \text{diam}(f(s))$.
AntilipschitzWith.id theorem
: AntilipschitzWith 1 (id : α → α)
Full source 
protected theorem id : AntilipschitzWith 1 (id : α → α) := fun x y => by
  simp only [ENNReal.coe_one, one_mul, id, le_refl]
Identity Function is Antilipschitz with Constant 1
Informal description
The identity function $\mathrm{id} \colon \alpha \to \alpha$ on an extended pseudo-metric space $\alpha$ is antilipschitz with constant $1$. That is, for all $x, y \in \alpha$, the extended distance satisfies $\text{edist}(x, y) \leq 1 \cdot \text{edist}(\mathrm{id}(x), \mathrm{id}(y)) = \text{edist}(x, y)$.
AntilipschitzWith.comp theorem
{Kg : ℝ≥0} {g : β → γ} (hg : AntilipschitzWith Kg g) {Kf : ℝ≥0} {f : α → β} (hf : AntilipschitzWith Kf f) : AntilipschitzWith (Kf * Kg) (g ∘ f)
Full source 
theorem comp {Kg : ℝ≥0} {g : β → γ} (hg : AntilipschitzWith Kg g) {Kf : ℝ≥0} {f : α → β}
    (hf : AntilipschitzWith Kf f) : AntilipschitzWith (Kf * Kg) (g ∘ f) := fun x y =>
  calc
    edist x y ≤ Kf * edist (f x) (f y) := hf x y
    _ ≤ Kf * (Kg * edist (g (f x)) (g (f y))) := mul_left_mono (hg _ _)
    _ = _ := by rw [ENNReal.coe_mul, mul_assoc]; rfl
Composition of Antilipschitz Functions with Constant $K_f \cdot K_g$
Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be antilipschitz functions between extended pseudo-metric spaces with constants $K_f \geq 0$ and $K_g \geq 0$ respectively. Then their composition $g \circ f \colon \alpha \to \gamma$ is antilipschitz with constant $K_f \cdot K_g$.
AntilipschitzWith.restrict theorem
(hf : AntilipschitzWith K f) (s : Set α) : AntilipschitzWith K (s.restrict f)
Full source 
theorem restrict (hf : AntilipschitzWith K f) (s : Set α) : AntilipschitzWith K (s.restrict f) :=
  fun x y => hf x y
Restriction of Antilipschitz Function Preserves Constant
Informal description
Let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$ between two extended pseudo-metric spaces. For any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ is also antilipschitz with the same constant $K$.
AntilipschitzWith.codRestrict theorem
(hf : AntilipschitzWith K f) {s : Set β} (hs : ∀ x, f x ∈ s) : AntilipschitzWith K (s.codRestrict f hs)
Full source 
theorem codRestrict (hf : AntilipschitzWith K f) {s : Set β} (hs : ∀ x, f x ∈ s) :
    AntilipschitzWith K (s.codRestrict f hs) := fun x y => hf x y
Codomain Restriction Preserves Antilipschitz Property
Informal description
Let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$ between two extended pseudo-metric spaces, and let $s \subseteq \beta$ be a subset such that $f(x) \in s$ for all $x \in \alpha$. Then the codomain-restricted function $\mathrm{codRestrict}\, f\, s\, hs \colon \alpha \to s$ is also antilipschitz with the same constant $K$.
AntilipschitzWith.to_rightInvOn' theorem
{s : Set α} (hf : AntilipschitzWith K (s.restrict f)) {g : β → α} {t : Set β} (g_maps : MapsTo g t s) (g_inv : RightInvOn g f t) : LipschitzWith K (t.restrict g)
Full source 
theorem to_rightInvOn' {s : Set α} (hf : AntilipschitzWith K (s.restrict f)) {g : β → α}
    {t : Set β} (g_maps : MapsTo g t s) (g_inv : RightInvOn g f t) :
    LipschitzWith K (t.restrict g) := fun x y => by
  simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, Subtype.edist_mk_mk]
    using hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩
Lipschitz property of right inverses to antilipschitz restrictions
Informal description
Let $f \colon \alpha \to \beta$ be a function between extended pseudo-metric spaces, and let $s \subseteq \alpha$ be a subset such that the restriction $f|_s$ is antilipschitz with constant $K \geq 0$. Suppose $g \colon \beta \to \alpha$ is a function mapping a subset $t \subseteq \beta$ into $s$, and $g$ is a right inverse of $f$ on $t$ (i.e., $f(g(x)) = x$ for all $x \in t$). Then the restriction $g|_t$ is lipschitz with constant $K$.
AntilipschitzWith.to_rightInvOn theorem
(hf : AntilipschitzWith K f) {g : β → α} {t : Set β} (h : RightInvOn g f t) : LipschitzWith K (t.restrict g)
Full source 
theorem to_rightInvOn (hf : AntilipschitzWith K f) {g : β → α} {t : Set β} (h : RightInvOn g f t) :
    LipschitzWith K (t.restrict g) :=
  (hf.restrict univ).to_rightInvOn' (mapsTo_univ g t) h
Lipschitz property of right inverses to antilipschitz functions on subsets
Informal description
Let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$ between two extended pseudo-metric spaces. If $g \colon \beta \to \alpha$ is a right inverse of $f$ on a subset $t \subseteq \beta$ (i.e., $f(g(x)) = x$ for all $x \in t$), then the restriction of $g$ to $t$ is a Lipschitz function with constant $K$.
AntilipschitzWith.to_rightInverse theorem
(hf : AntilipschitzWith K f) {g : β → α} (hg : Function.RightInverse g f) : LipschitzWith K g
Full source 
theorem to_rightInverse (hf : AntilipschitzWith K f) {g : β → α} (hg : Function.RightInverse g f) :
    LipschitzWith K g := by
  intro x y
  have := hf (g x) (g y)
  rwa [hg x, hg y] at this
Right Inverse of Antilipschitz Function is Lipschitz with Same Constant
Informal description
Let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$ between two extended pseudo-metric spaces. If $g \colon \beta \to \alpha$ is a right inverse of $f$ (i.e., $f \circ g = \text{id}_\beta$), then $g$ is a Lipschitz function with constant $K$.
AntilipschitzWith.comap_uniformity_le theorem
(hf : AntilipschitzWith K f) : (𝓤 β).comap (Prod.map f f) ≤ 𝓤 α
Full source 
theorem comap_uniformity_le (hf : AntilipschitzWith K f) : (𝓤 β).comap (Prod.map f f) ≤ 𝓤 α := by
  refine ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 fun ε h₀ => ?_
  refine ⟨(↑K)⁻¹ * ε, ENNReal.mul_pos (ENNReal.inv_ne_zero.2 ENNReal.coe_ne_top) h₀.ne', ?_⟩
  refine fun x hx => (hf x.1 x.2).trans_lt ?_
  rw [mul_comm, ← div_eq_mul_inv] at hx
  rw [mul_comm]
  exact ENNReal.mul_lt_of_lt_div hx
Uniformity Filter Comparison for Antilipschitz Functions
Informal description
Let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$ between two extended pseudo-metric spaces. Then the uniformity filter on $\beta$ pulled back via $f \times f$ is finer than the uniformity filter on $\alpha$, i.e., \[ \text{comap}_{f \times f}(\mathfrak{U}(\beta)) \leq \mathfrak{U}(\alpha), \] where $\mathfrak{U}(\alpha)$ and $\mathfrak{U}(\beta)$ denote the uniformity filters on $\alpha$ and $\beta$ respectively.
AntilipschitzWith.isUniformInducing theorem
(hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsUniformInducing f
Full source 
theorem isUniformInducing (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) :
    IsUniformInducing f :=
  ⟨le_antisymm hf.comap_uniformity_le hfc.le_comap⟩
Uniform Inducing Property of Antilipschitz and Uniformly Continuous Functions
Informal description
Let $f \colon \alpha \to \beta$ be a function between two extended pseudo-metric spaces that is antilipschitz with constant $K \geq 0$ and uniformly continuous. Then $f$ is a uniform inducing map, meaning the uniformity filter on $\alpha$ is the pullback of the uniformity filter on $\beta$ under the product map $f \times f$.
AntilipschitzWith.isUniformEmbedding theorem
{α β : Type*} [EMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0} {f : α → β} (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsUniformEmbedding f
Full source 
lemma isUniformEmbedding {α β : Type*} [EMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0} {f : α → β}
    (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsUniformEmbedding f :=
  ⟨hf.isUniformInducing hfc, hf.injective⟩
Uniform Embedding Property of Antilipschitz and Uniformly Continuous Functions
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, with $\alpha$ being an extended metric space (i.e., the distance separates points). Let $f \colon \alpha \to \beta$ be a function that is antilipschitz with constant $K \geq 0$ and uniformly continuous. Then $f$ is a uniform embedding, meaning it is injective, uniformly continuous, and the uniformity on $\alpha$ is induced by $f$ from the uniformity on $\beta$.
AntilipschitzWith.isComplete_range theorem
[CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsComplete (range f)
Full source 
theorem isComplete_range [CompleteSpace α] (hf : AntilipschitzWith K f)
    (hfc : UniformContinuous f) : IsComplete (range f) :=
  (hf.isUniformInducing hfc).isComplete_range
Range of Antilipschitz and Uniformly Continuous Function from Complete Space is Complete
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, with $\alpha$ complete. If $f \colon \alpha \to \beta$ is an antilipschitz function with constant $K \geq 0$ and uniformly continuous, then the range of $f$ is a complete subset of $\beta$.
AntilipschitzWith.isClosed_range theorem
{α β : Type*} [PseudoEMetricSpace α] [EMetricSpace β] [CompleteSpace α] {f : α → β} {K : ℝ≥0} (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsClosed (range f)
Full source 
theorem isClosed_range {α β : Type*} [PseudoEMetricSpace α] [EMetricSpace β] [CompleteSpace α]
    {f : α → β} {K : ℝ≥0} (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) :
    IsClosed (range f) :=
  (hf.isComplete_range hfc).isClosed
Range of Antilipschitz and Uniformly Continuous Function from Complete Space is Closed
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, with $\alpha$ complete and $\beta$ an extended metric space. If $f \colon \alpha \to \beta$ is an antilipschitz function with constant $K \geq 0$ and uniformly continuous, then the range of $f$ is closed in $\beta$.
AntilipschitzWith.isClosedEmbedding theorem
{α : Type*} {β : Type*} [EMetricSpace α] [EMetricSpace β] {K : ℝ≥0} {f : α → β} [CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsClosedEmbedding f
Full source 
theorem isClosedEmbedding {α : Type*} {β : Type*} [EMetricSpace α] [EMetricSpace β] {K : ℝ≥0}
    {f : α → β} [CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) :
    IsClosedEmbedding f :=
  { (hf.isUniformEmbedding hfc).isEmbedding with isClosed_range := hf.isClosed_range hfc }
Closed Embedding Property of Antilipschitz and Uniformly Continuous Functions from Complete Spaces
Informal description
Let $\alpha$ and $\beta$ be extended metric spaces, with $\alpha$ complete. If a function $f \colon \alpha \to \beta$ is antilipschitz with constant $K \geq 0$ and uniformly continuous, then $f$ is a closed embedding. That is, $f$ is injective, continuous, and maps closed sets in $\alpha$ to closed sets in $\beta$ (relative to the subspace topology on the image of $f$).
AntilipschitzWith.subtype_coe theorem
(s : Set α) : AntilipschitzWith 1 ((↑) : s → α)
Full source 
theorem subtype_coe (s : Set α) : AntilipschitzWith 1 ((↑) : s → α) :=
  AntilipschitzWith.id.restrict s
Inclusion Map is Antilipschitz with Constant 1
Informal description
For any subset $s$ of an extended pseudo-metric space $\alpha$, the inclusion map $\iota \colon s \to \alpha$ (which sends each element of $s$ to itself in $\alpha$) is antilipschitz with constant $1$. That is, for all $x, y \in s$, the extended distance satisfies $\text{edist}(x, y) \leq 1 \cdot \text{edist}(\iota(x), \iota(y)) = \text{edist}(x, y)$.
AntilipschitzWith.of_subsingleton theorem
[Subsingleton α] {K : ℝ≥0} : AntilipschitzWith K f
Full source 
@[nontriviality]
theorem of_subsingleton [Subsingleton α] {K : ℝ≥0} : AntilipschitzWith K f := fun x y => by
  simp only [Subsingleton.elim x y, edist_self, zero_le]
Antilipschitz property for functions from subsingleton spaces
Informal description
For any subsingleton type $\alpha$ (i.e., a type with at most one element) and any extended pseudo-metric space $\beta$, every function $f \colon \alpha \to \beta$ is antilipschitz with any constant $K \geq 0$. That is, for all $x, y \in \alpha$, the inequality $\text{edist}(x, y) \leq K \cdot \text{edist}(f(x), f(y))$ holds trivially.
AntilipschitzWith.subsingleton theorem
{α β} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : AntilipschitzWith 0 f) : Subsingleton α
Full source 
/-- If `f : α → β` is `0`-antilipschitz, then `α` is a `subsingleton`. -/
protected theorem subsingleton {α β} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β}
    (h : AntilipschitzWith 0 f) : Subsingleton α :=
  ⟨fun x y => edist_le_zero.1 <| (h x y).trans_eq <| zero_mul _⟩
$0$-Antilipschitz Functions Imply Subsingleton Domain
Informal description
Let $\alpha$ be an extended metric space and $\beta$ a pseudo-extended metric space. If a function $f \colon \alpha \to \beta$ is $0$-antilipschitz (i.e., satisfies $\text{edist}(x, y) \leq 0 \cdot \text{edist}(f(x), f(y))$ for all $x, y \in \alpha$), then $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal).
AntilipschitzWith.isBounded_preimage theorem
(hf : AntilipschitzWith K f) {s : Set β} (hs : IsBounded s) : IsBounded (f ⁻¹' s)
Full source 
theorem isBounded_preimage (hf : AntilipschitzWith K f) {s : Set β} (hs : IsBounded s) :
    IsBounded (f ⁻¹' s) :=
  isBounded_iff_ediam_ne_top.2 <| ne_top_of_le_ne_top
    (ENNReal.mul_ne_top ENNReal.coe_ne_top hs.ediam_ne_top) (hf.ediam_preimage_le _)
Boundedness of Preimage under Antilipschitz Map
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$. For any bounded subset $s \subseteq \beta$, the preimage $f^{-1}(s)$ is bounded in $\alpha$.
AntilipschitzWith.tendsto_cobounded theorem
(hf : AntilipschitzWith K f) : Tendsto f (cobounded α) (cobounded β)
Full source 
theorem tendsto_cobounded (hf : AntilipschitzWith K f) : Tendsto f (cobounded α) (cobounded β) :=
  compl_surjective.forall.2 fun _ ↦ hf.isBounded_preimage
Antilipschitz functions preserve co-boundedness
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta$ be an antilipschitz function with constant $K \geq 0$. Then $f$ maps co-bounded sets in $\alpha$ to co-bounded sets in $\beta$, i.e., the function $f$ tends to co-boundedness in the sense that for any co-bounded set $S \subseteq \alpha$, the image $f(S)$ is co-bounded in $\beta$.
AntilipschitzWith.properSpace theorem
{α : Type*} [MetricSpace α] {K : ℝ≥0} {f : α → β} [ProperSpace α] (hK : AntilipschitzWith K f) (f_cont : Continuous f) (hf : Function.Surjective f) : ProperSpace β
Full source 
/-- The image of a proper space under an expanding onto map is proper. -/
protected theorem properSpace {α : Type*} [MetricSpace α] {K : ℝ≥0} {f : α → β} [ProperSpace α]
    (hK : AntilipschitzWith K f) (f_cont : Continuous f) (hf : Function.Surjective f) :
    ProperSpace β := by
  refine ⟨fun x₀ r => ?_⟩
  let K := f ⁻¹' closedBall x₀ r
  have A : IsClosed K := isClosed_closedBall.preimage f_cont
  have B : IsBounded K := hK.isBounded_preimage isBounded_closedBall
  have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩
  convert this.image f_cont
  exact (hf.image_preimage _).symm
Properness of Codomain under Continuous Surjective Antilipschitz Map
Informal description
Let $\alpha$ and $\beta$ be metric spaces, with $\alpha$ being proper. If $f \colon \alpha \to \beta$ is a continuous, surjective, and antilipschitz function with constant $K \geq 0$, then $\beta$ is also a proper metric space.
AntilipschitzWith.isBounded_of_image2_left theorem
(f : α → β → γ) {K₁ : ℝ≥0} (hf : ∀ b, AntilipschitzWith K₁ fun a => f a b) {s : Set α} {t : Set β} (hst : IsBounded (Set.image2 f s t)) : IsBounded s ∨ IsBounded t
Full source 
theorem isBounded_of_image2_left (f : α → β → γ) {K₁ : ℝ≥0}
    (hf : ∀ b, AntilipschitzWith K₁ fun a => f a b) {s : Set α} {t : Set β}
    (hst : IsBounded (Set.image2 f s t)) : IsBoundedIsBounded s ∨ IsBounded t := by
  contrapose! hst
  obtain ⟨b, hb⟩ : t.Nonempty := nonempty_of_not_isBounded hst.2
  have : ¬IsBounded (Set.image2 f s {b}) := by
    intro h
    apply hst.1
    rw [Set.image2_singleton_right] at h
    replace h := (hf b).isBounded_preimage h
    exact h.subset (subset_preimage_image _ _)
  exact mt (IsBounded.subset · (image2_subset subset_rfl (singleton_subset_iff.mpr hb))) this
Boundedness of Partial Antilipschitz Function's Domain from Bounded Image
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta \to \gamma$ be a function such that for every fixed $b \in \beta$, the partial function $f(\cdot, b) \colon \alpha \to \gamma$ is antilipschitz with constant $K_1 \geq 0$. If the image $\{f(a, b) \mid a \in s, b \in t\}$ is bounded in $\gamma$, then either $s$ is bounded in $\alpha$ or $t$ is bounded in $\beta$.
AntilipschitzWith.isBounded_of_image2_right theorem
{f : α → β → γ} {K₂ : ℝ≥0} (hf : ∀ a, AntilipschitzWith K₂ (f a)) {s : Set α} {t : Set β} (hst : IsBounded (Set.image2 f s t)) : IsBounded s ∨ IsBounded t
Full source 
theorem isBounded_of_image2_right {f : α → β → γ} {K₂ : ℝ≥0} (hf : ∀ a, AntilipschitzWith K₂ (f a))
    {s : Set α} {t : Set β} (hst : IsBounded (Set.image2 f s t)) : IsBoundedIsBounded s ∨ IsBounded t :=
  Or.symm <| isBounded_of_image2_left (flip f) hf <| image2_swap f s t ▸ hst
Boundedness of Partial Antilipschitz Function's Codomain from Bounded Image
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta \to \gamma$ be a function such that for every fixed $a \in \alpha$, the partial function $f(a, \cdot) \colon \beta \to \gamma$ is antilipschitz with constant $K_2 \geq 0$. If the image $\{f(a, b) \mid a \in s, b \in t\}$ is bounded in $\gamma$, then either $s$ is bounded in $\alpha$ or $t$ is bounded in $\beta$.
LipschitzWith.to_rightInverse theorem
[PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0} {f : α → β} (hf : LipschitzWith K f) {g : β → α} (hg : Function.RightInverse g f) : AntilipschitzWith K g
Full source 
theorem LipschitzWith.to_rightInverse [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0}
    {f : α → β} (hf : LipschitzWith K f) {g : β → α} (hg : Function.RightInverse g f) :
    AntilipschitzWith K g := fun x y => by simpa only [hg _] using hf (g x) (g y)
Right inverse of a Lipschitz function is antilipschitz with the same constant
Informal description
Let $\alpha$ and $\beta$ be extended pseudo-metric spaces, and let $f \colon \alpha \to \beta$ be a Lipschitz function with constant $K \geq 0$. If $g \colon \beta \to \alpha$ is a right inverse of $f$ (i.e., $f \circ g = \text{id}_\beta$), then $g$ is antilipschitz with the same constant $K$.