doc-next-gen

Mathlib.Topology.MetricSpace.Isometry

Module docstring

{"# Isometries

We define isometries, i.e., maps between emetric spaces that preserve the edistance (on metric spaces, these are exactly the maps that preserve distances), and prove their basic properties. We also introduce isometric bijections.

Since a lot of elementary properties don't require eq_of_dist_eq_zero we start setting up the theory for PseudoMetricSpace and we specialize to MetricSpace when needed. "}

Isometry definition
[PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) : Prop
Full source 
/-- An isometry (also known as isometric embedding) is a map preserving the edistance
between pseudoemetric spaces, or equivalently the distance between pseudometric space. -/
def Isometry [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) : Prop :=
  ∀ x1 x2 : α, edist (f x1) (f x2) = edist x1 x2
Isometry (distance-preserving map)
Informal description
A function \( f \) between two pseudoemetric spaces \( \alpha \) and \( \beta \) is called an isometry if it preserves the extended distance, i.e., for any \( x_1, x_2 \in \alpha \), the extended distance between \( f(x_1) \) and \( f(x_2) \) in \( \beta \) is equal to the extended distance between \( x_1 \) and \( x_2 \) in \( \alpha \).
isometry_iff_nndist_eq theorem
[PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : Isometry f ↔ ∀ x y, nndist (f x) (f y) = nndist x y
Full source 
/-- On pseudometric spaces, a map is an isometry if and only if it preserves nonnegative
distances. -/
theorem isometry_iff_nndist_eq [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} :
    IsometryIsometry f ↔ ∀ x y, nndist (f x) (f y) = nndist x y := by
  simp only [Isometry, edist_nndist, ENNReal.coe_inj]
Isometry Characterization via Nonnegative Distance Preservation
Informal description
Let $\alpha$ and $\beta$ be pseudometric spaces. A function $f \colon \alpha \to \beta$ is an isometry if and only if it preserves the nonnegative distance, i.e., for all $x, y \in \alpha$, the nonnegative distance between $f(x)$ and $f(y)$ equals the nonnegative distance between $x$ and $y$: \[ \text{nndist}(f(x), f(y)) = \text{nndist}(x, y). \]
isometry_iff_dist_eq theorem
[PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : Isometry f ↔ ∀ x y, dist (f x) (f y) = dist x y
Full source 
/-- On pseudometric spaces, a map is an isometry if and only if it preserves distances. -/
theorem isometry_iff_dist_eq [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} :
    IsometryIsometry f ↔ ∀ x y, dist (f x) (f y) = dist x y := by
  simp only [isometry_iff_nndist_eq, ← coe_nndist, NNReal.coe_inj]
Distance-Preserving Characterization of Isometries on Pseudometric Spaces
Informal description
A function $f \colon \alpha \to \beta$ between pseudometric spaces is an isometry if and only if it preserves distances, i.e., for all $x, y \in \alpha$, the distance between $f(x)$ and $f(y)$ in $\beta$ equals the distance between $x$ and $y$ in $\alpha$: \[ \text{dist}(f(x), f(y)) = \text{dist}(x, y). \]
Isometry.edist_eq theorem
(hf : Isometry f) (x y : α) : edist (f x) (f y) = edist x y
Full source 
/-- An isometry preserves edistances. -/
theorem edist_eq (hf : Isometry f) (x y : α) : edist (f x) (f y) = edist x y :=
  hf x y
Isometry Preserves Extended Distance
Informal description
Let \( f \) be an isometry between two pseudoemetric spaces \( \alpha \) and \( \beta \). Then for any two points \( x, y \in \alpha \), the extended distance between \( f(x) \) and \( f(y) \) in \( \beta \) is equal to the extended distance between \( x \) and \( y \) in \( \alpha \), i.e., \[ \text{edist}(f(x), f(y)) = \text{edist}(x, y). \]
Isometry.lipschitz theorem
(h : Isometry f) : LipschitzWith 1 f
Full source 
theorem lipschitz (h : Isometry f) : LipschitzWith 1 f :=
  LipschitzWith.of_edist_le fun x y => (h x y).le
Isometries are 1-Lipschitz
Informal description
If $f \colon \alpha \to \beta$ is an isometry between pseudoemetric spaces, then $f$ is a Lipschitz function with Lipschitz constant $1$, i.e., for all $x, y \in \alpha$, \[ \text{edist}(f(x), f(y)) \leq \text{edist}(x, y). \]
Isometry.antilipschitz theorem
(h : Isometry f) : AntilipschitzWith 1 f
Full source 
theorem antilipschitz (h : Isometry f) : AntilipschitzWith 1 f := fun x y => by
  simp only [h x y, ENNReal.coe_one, one_mul, le_refl]
Isometries are 1-Antilipschitz
Informal description
If $f \colon \alpha \to \beta$ is an isometry between pseudoemetric spaces, then $f$ is an antilipschitz function with constant $1$, i.e., for all $x, y \in \alpha$, \[ \text{edist}(x, y) \leq \text{edist}(f(x), f(y)). \]
isometry_subsingleton theorem
[Subsingleton α] : Isometry f
Full source 
/-- Any map on a subsingleton is an isometry -/
@[nontriviality]
theorem _root_.isometry_subsingleton [Subsingleton α] : Isometry f := fun x y => by
  rw [Subsingleton.elim x y]; simp
Any Function on a Subsingleton is an Isometry
Informal description
Let $\alpha$ be a type with at most one element (i.e., a subsingleton) and $\beta$ be a pseudoemetric space. Then any function $f \colon \alpha \to \beta$ is an isometry, meaning it preserves the extended distance between points.
isometry_id theorem
: Isometry (id : α → α)
Full source 
/-- The identity is an isometry -/
theorem _root_.isometry_id : Isometry (id : α → α) := fun _ _ => rfl
Identity Map is an Isometry
Informal description
The identity map $\mathrm{id} \colon \alpha \to \alpha$ on a pseudoemetric space $\alpha$ is an isometry, i.e., it preserves the extended distance between any two points $x_1, x_2 \in \alpha$.
Isometry.prodMap theorem
{δ} [PseudoEMetricSpace δ] {f : α → β} {g : γ → δ} (hf : Isometry f) (hg : Isometry g) : Isometry (Prod.map f g)
Full source 
theorem prodMap {δ} [PseudoEMetricSpace δ] {f : α → β} {g : γ → δ} (hf : Isometry f)
    (hg : Isometry g) : Isometry (Prod.map f g) := fun x y => by
  simp only [Prod.edist_eq, Prod.map_fst, hf.edist_eq, Prod.map_snd, hg.edist_eq]
Product of Isometries is an Isometry
Informal description
Let $\alpha$, $\beta$, $\gamma$, and $\delta$ be pseudoemetric spaces. Given isometries $f \colon \alpha \to \beta$ and $g \colon \gamma \to \delta$, the product map $f \times g \colon \alpha \times \gamma \to \beta \times \delta$ defined by $(x, y) \mapsto (f(x), g(y))$ is also an isometry.
Isometry.piMap theorem
{ι} [Fintype ι] {α β : ι → Type*} [∀ i, PseudoEMetricSpace (α i)] [∀ i, PseudoEMetricSpace (β i)] (f : ∀ i, α i → β i) (hf : ∀ i, Isometry (f i)) : Isometry (Pi.map f)
Full source 
protected theorem piMap {ι} [Fintype ι] {α β : ι → Type*} [∀ i, PseudoEMetricSpace (α i)]
    [∀ i, PseudoEMetricSpace (β i)] (f : ∀ i, α i → β i) (hf : ∀ i, Isometry (f i)) :
    Isometry (Pi.map f) := fun x y => by
  simp only [edist_pi_def, (hf _).edist_eq, Pi.map_apply]
Component-wise Isometry Preserves Extended Distance in Product Spaces
Informal description
Let $\iota$ be a finite index set, and for each $i \in \iota$, let $\alpha_i$ and $\beta_i$ be pseudoemetric spaces. Given a family of functions $f_i \colon \alpha_i \to \beta_i$ such that each $f_i$ is an isometry, the component-wise application function $\mathrm{Pi.map} \, f \colon \prod_{i \in \iota} \alpha_i \to \prod_{i \in \iota} \beta_i$ is also an isometry. That is, for any $x, y \in \prod_{i \in \iota} \alpha_i$, the extended distance between $\mathrm{Pi.map} \, f \, x$ and $\mathrm{Pi.map} \, f \, y$ equals the extended distance between $x$ and $y$.
Isometry.comp theorem
{g : β → γ} {f : α → β} (hg : Isometry g) (hf : Isometry f) : Isometry (g ∘ f)
Full source 
/-- The composition of isometries is an isometry. -/
theorem comp {g : β → γ} {f : α → β} (hg : Isometry g) (hf : Isometry f) : Isometry (g ∘ f) :=
  fun _ _ => (hg _ _).trans (hf _ _)
Composition of Isometries is an Isometry
Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be isometries between pseudoemetric spaces. Then the composition $g \circ f \colon \alpha \to \gamma$ is also an isometry.
Isometry.uniformContinuous theorem
(hf : Isometry f) : UniformContinuous f
Full source 
/-- An isometry from a metric space is a uniform continuous map -/
protected theorem uniformContinuous (hf : Isometry f) : UniformContinuous f :=
  hf.lipschitz.uniformContinuous
Isometries are uniformly continuous
Informal description
If $f \colon \alpha \to \beta$ is an isometry between pseudoemetric spaces, then $f$ is uniformly continuous.
Isometry.isUniformInducing theorem
(hf : Isometry f) : IsUniformInducing f
Full source 
/-- An isometry from a metric space is a uniform inducing map -/
theorem isUniformInducing (hf : Isometry f) : IsUniformInducing f :=
  hf.antilipschitz.isUniformInducing hf.uniformContinuous
Isometries are Uniformly Inducing Maps
Informal description
If $f \colon \alpha \to \beta$ is an isometry between pseudoemetric spaces, 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$.
Isometry.tendsto_nhds_iff theorem
{ι : Type*} {f : α → β} {g : ι → α} {a : Filter ι} {b : α} (hf : Isometry f) : Filter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto (f ∘ g) a (𝓝 (f b))
Full source 
theorem tendsto_nhds_iff {ι : Type*} {f : α → β} {g : ι → α} {a : Filter ι} {b : α}
    (hf : Isometry f) : Filter.TendstoFilter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto (f ∘ g) a (𝓝 (f b)) :=
  hf.isUniformInducing.isInducing.tendsto_nhds_iff
Limit Characterization via Isometry: $\lim g = b \leftrightarrow \lim (f \circ g) = f(b)$
Informal description
Let $f \colon \alpha \to \beta$ be an isometry between pseudoemetric spaces, and let $g \colon \iota \to \alpha$ be a function. For any filter $a$ on $\iota$ and any point $b \in \alpha$, the function $g$ tends to $b$ along $a$ if and only if the composition $f \circ g$ tends to $f(b)$ along $a$. In other words, $\lim_{a} g = b$ if and only if $\lim_{a} (f \circ g) = f(b)$.
Isometry.continuous theorem
(hf : Isometry f) : Continuous f
Full source 
/-- An isometry is continuous. -/
protected theorem continuous (hf : Isometry f) : Continuous f :=
  hf.lipschitz.continuous
Continuity of Isometries
Informal description
If $f \colon \alpha \to \beta$ is an isometry between pseudoemetric spaces, then $f$ is continuous.
Isometry.right_inv theorem
{f : α → β} {g : β → α} (h : Isometry f) (hg : RightInverse g f) : Isometry g
Full source 
/-- The right inverse of an isometry is an isometry. -/
theorem right_inv {f : α → β} {g : β → α} (h : Isometry f) (hg : RightInverse g f) : Isometry g :=
  fun x y => by rw [← h, hg _, hg _]
Right Inverse of an Isometry is an Isometry
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudoemetric spaces $\alpha$ and $\beta$, and let $g : \beta \to \alpha$ be a right inverse of $f$. Then $g$ is also an isometry.
Isometry.preimage_emetric_closedBall theorem
(h : Isometry f) (x : α) (r : ℝ≥0∞) : f ⁻¹' EMetric.closedBall (f x) r = EMetric.closedBall x r
Full source 
theorem preimage_emetric_closedBall (h : Isometry f) (x : α) (r : ℝ≥0∞) :
    f ⁻¹' EMetric.closedBall (f x) r = EMetric.closedBall x r := by
  ext y
  simp [h.edist_eq]
Preimage of Closed Ball under Isometry Equals Closed Ball
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudoemetric spaces $\alpha$ and $\beta$. For any point $x \in \alpha$ and any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage under $f$ of the closed ball centered at $f(x)$ with radius $r$ in $\beta$ is equal to the closed ball centered at $x$ with radius $r$ in $\alpha$. That is, \[ f^{-1}(\overline{B}(f(x), r)) = \overline{B}(x, r). \]
Isometry.preimage_emetric_ball theorem
(h : Isometry f) (x : α) (r : ℝ≥0∞) : f ⁻¹' EMetric.ball (f x) r = EMetric.ball x r
Full source 
theorem preimage_emetric_ball (h : Isometry f) (x : α) (r : ℝ≥0∞) :
    f ⁻¹' EMetric.ball (f x) r = EMetric.ball x r := by
  ext y
  simp [h.edist_eq]
Preimage of Open Ball under Isometry Equals Open Ball
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudoemetric spaces $\alpha$ and $\beta$. For any point $x \in \alpha$ and any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage under $f$ of the open ball centered at $f(x)$ with radius $r$ in $\beta$ is equal to the open ball centered at $x$ with radius $r$ in $\alpha$. In other words, \[ f^{-1}\big(B(f(x), r)\big) = B(x, r). \]
Isometry.ediam_image theorem
(hf : Isometry f) (s : Set α) : EMetric.diam (f '' s) = EMetric.diam s
Full source 
/-- Isometries preserve the diameter in pseudoemetric spaces. -/
theorem ediam_image (hf : Isometry f) (s : Set α) : EMetric.diam (f '' s) = EMetric.diam s :=
  eq_of_forall_ge_iff fun d => by simp only [EMetric.diam_le_iff, forall_mem_image, hf.edist_eq]
Isometry Preserves Extended Diameter of Subsets
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudoemetric spaces $\alpha$ and $\beta$. For any subset $s \subseteq \alpha$, the extended diameter of the image $f(s)$ in $\beta$ is equal to the extended diameter of $s$ in $\alpha$, i.e., \[ \text{diam}(f(s)) = \text{diam}(s). \]
Isometry.ediam_range theorem
(hf : Isometry f) : EMetric.diam (range f) = EMetric.diam (univ : Set α)
Full source 
theorem ediam_range (hf : Isometry f) : EMetric.diam (range f) = EMetric.diam (univ : Set α) := by
  rw [← image_univ]
  exact hf.ediam_image univ
Isometry Preserves Extended Diameter of Range and Universal Set
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudoemetric spaces $\alpha$ and $\beta$. Then the extended diameter of the range of $f$ is equal to the extended diameter of the universal set in $\alpha$, i.e., \[ \text{diam}(\text{range}(f)) = \text{diam}(\text{univ}). \]
Isometry.mapsTo_emetric_ball theorem
(hf : Isometry f) (x : α) (r : ℝ≥0∞) : MapsTo f (EMetric.ball x r) (EMetric.ball (f x) r)
Full source 
theorem mapsTo_emetric_ball (hf : Isometry f) (x : α) (r : ℝ≥0∞) :
    MapsTo f (EMetric.ball x r) (EMetric.ball (f x) r) :=
  (hf.preimage_emetric_ball x r).ge
Isometry Maps Open Balls into Open Balls
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudoemetric spaces $\alpha$ and $\beta$. For any point $x \in \alpha$ and any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the image of the open ball $B(x, r)$ under $f$ is contained in the open ball $B(f(x), r)$. In other words, \[ f(B(x, r)) \subseteq B(f(x), r). \]
Isometry.mapsTo_emetric_closedBall theorem
(hf : Isometry f) (x : α) (r : ℝ≥0∞) : MapsTo f (EMetric.closedBall x r) (EMetric.closedBall (f x) r)
Full source 
theorem mapsTo_emetric_closedBall (hf : Isometry f) (x : α) (r : ℝ≥0∞) :
    MapsTo f (EMetric.closedBall x r) (EMetric.closedBall (f x) r) :=
  (hf.preimage_emetric_closedBall x r).ge
Isometry Maps Closed Balls to Closed Balls
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudoemetric spaces $\alpha$ and $\beta$. For any point $x \in \alpha$ and any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the image under $f$ of the closed ball centered at $x$ with radius $r$ in $\alpha$ is contained in the closed ball centered at $f(x)$ with radius $r$ in $\beta$. That is, \[ f(\overline{B}(x, r)) \subseteq \overline{B}(f(x), r). \]
isometry_subtype_coe theorem
{s : Set α} : Isometry ((↑) : s → α)
Full source 
/-- The injection from a subtype is an isometry -/
theorem _root_.isometry_subtype_coe {s : Set α} : Isometry ((↑) : s → α) := fun _ _ => rfl
Canonical Inclusion is an Isometry on Subsets
Informal description
For any subset $s$ of a pseudoemetric space $\alpha$, the canonical inclusion map from $s$ to $\alpha$ (denoted by the coercion symbol $\uparrow$) is an isometry. That is, for any $x, y \in s$, the extended distance between $x$ and $y$ in $\alpha$ is equal to the extended distance between $\uparrow x$ and $\uparrow y$ in $\alpha$.
Isometry.comp_continuousOn_iff theorem
{γ} [TopologicalSpace γ] (hf : Isometry f) {g : γ → α} {s : Set γ} : ContinuousOn (f ∘ g) s ↔ ContinuousOn g s
Full source 
theorem comp_continuousOn_iff {γ} [TopologicalSpace γ] (hf : Isometry f) {g : γ → α} {s : Set γ} :
    ContinuousOnContinuousOn (f ∘ g) s ↔ ContinuousOn g s :=
  hf.isUniformInducing.isInducing.continuousOn_iff.symm
Continuity of Composition with Isometry on Subsets
Informal description
Let $f \colon \alpha \to \beta$ be an isometry between pseudoemetric spaces, and let $g \colon \gamma \to \alpha$ be a function from a topological space $\gamma$. For any subset $s \subseteq \gamma$, the composition $f \circ g$ is continuous on $s$ if and only if $g$ is continuous on $s$.
Isometry.comp_continuous_iff theorem
{γ} [TopologicalSpace γ] (hf : Isometry f) {g : γ → α} : Continuous (f ∘ g) ↔ Continuous g
Full source 
theorem comp_continuous_iff {γ} [TopologicalSpace γ] (hf : Isometry f) {g : γ → α} :
    ContinuousContinuous (f ∘ g) ↔ Continuous g :=
  hf.isUniformInducing.isInducing.continuous_iff.symm
Continuity of Composition with Isometry: $f \circ g$ Continuous $\leftrightarrow$ $g$ Continuous
Informal description
Let $\alpha$ and $\beta$ be pseudoemetric spaces, and let $f \colon \alpha \to \beta$ be an isometry. For any topological space $\gamma$ and any function $g \colon \gamma \to \alpha$, the composition $f \circ g$ is continuous if and only if $g$ is continuous.
Isometry.injective theorem
(h : Isometry f) : Injective f
Full source 
/-- An isometry from an emetric space is injective -/
protected theorem injective (h : Isometry f) : Injective f :=
  h.antilipschitz.injective
Injectivity of Isometries
Informal description
An isometry $f \colon \alpha \to \beta$ between pseudoemetric spaces is injective, i.e., for any $x, y \in \alpha$, if $f(x) = f(y)$, then $x = y$.
Isometry.isUniformEmbedding theorem
(hf : Isometry f) : IsUniformEmbedding f
Full source 
/-- An isometry from an emetric space is a uniform embedding -/
lemma isUniformEmbedding (hf : Isometry f) : IsUniformEmbedding f :=
  hf.antilipschitz.isUniformEmbedding hf.lipschitz.uniformContinuous
Isometries are Uniform Embeddings
Informal description
An isometry $f \colon \alpha \to \beta$ between pseudoemetric spaces is a uniform embedding, meaning it is injective, uniformly continuous, and the uniformity on $\alpha$ is induced by $f$ from the uniformity on $\beta$.
Isometry.isEmbedding theorem
(hf : Isometry f) : IsEmbedding f
Full source 
/-- An isometry from an emetric space is an embedding -/
theorem isEmbedding (hf : Isometry f) : IsEmbedding f := hf.isUniformEmbedding.isEmbedding
Isometries are Topological Embeddings
Informal description
An isometry $f \colon \alpha \to \beta$ between pseudoemetric spaces is a topological embedding, i.e., it is injective and induces the topology on $\alpha$ from the topology on $\beta$.
Isometry.isClosedEmbedding theorem
[CompleteSpace α] [EMetricSpace γ] {f : α → γ} (hf : Isometry f) : IsClosedEmbedding f
Full source 
/-- An isometry from a complete emetric space is a closed embedding -/
theorem isClosedEmbedding [CompleteSpace α] [EMetricSpace γ] {f : α → γ} (hf : Isometry f) :
    IsClosedEmbedding f :=
  hf.antilipschitz.isClosedEmbedding hf.lipschitz.uniformContinuous
Isometries from Complete Spaces are Closed Embeddings
Informal description
Let $\alpha$ be a complete extended metric space and $\gamma$ be an extended metric space. If $f \colon \alpha \to \gamma$ is an isometry (i.e., a distance-preserving map), then $f$ is a closed embedding. That is, $f$ is injective, continuous, and maps closed sets in $\alpha$ to closed sets in $\gamma$ (relative to the subspace topology on the image of $f$).
Isometry.diam_image theorem
(hf : Isometry f) (s : Set α) : Metric.diam (f '' s) = Metric.diam s
Full source 
/-- An isometry preserves the diameter in pseudometric spaces. -/
theorem diam_image (hf : Isometry f) (s : Set α) : Metric.diam (f '' s) = Metric.diam s := by
  rw [Metric.diam, Metric.diam, hf.ediam_image]
Isometry Preserves Diameter of Subsets
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudometric spaces $\alpha$ and $\beta$. For any subset $s \subseteq \alpha$, the diameter of the image $f(s)$ in $\beta$ is equal to the diameter of $s$ in $\alpha$, i.e., \[ \text{diam}(f(s)) = \text{diam}(s). \]
Isometry.diam_range theorem
(hf : Isometry f) : Metric.diam (range f) = Metric.diam (univ : Set α)
Full source 
theorem diam_range (hf : Isometry f) : Metric.diam (range f) = Metric.diam (univ : Set α) := by
  rw [← image_univ]
  exact hf.diam_image univ
Isometry Preserves Diameter of Range and Universal Set
Informal description
Let $f : \alpha \to \beta$ be an isometry between two pseudometric spaces. Then the diameter of the range of $f$ is equal to the diameter of the universal set in $\alpha$, i.e., \[ \text{diam}(\text{range}(f)) = \text{diam}(\text{univ}). \]
Isometry.preimage_setOf_dist theorem
(hf : Isometry f) (x : α) (p : ℝ → Prop) : f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}
Full source 
theorem preimage_setOf_dist (hf : Isometry f) (x : α) (p : ℝ → Prop) :
    f ⁻¹' { y | p (dist y (f x)) } = { y | p (dist y x) } := by
  ext y
  simp [hf.dist_eq]
Isometry Preserves Distance Preimages: $f^{-1}\{y \mid p(d(y, f(x)))\} = \{y \mid p(d(y, x))\}$
Informal description
Let $f : \alpha \to \beta$ be an isometry between pseudometric spaces, and let $x \in \alpha$. For any predicate $p : \mathbb{R} \to \mathrm{Prop}$, the preimage under $f$ of the set $\{y \mid p(\mathrm{dist}(y, f(x)))\}$ is equal to the set $\{y \mid p(\mathrm{dist}(y, x))\}$.
Isometry.preimage_closedBall theorem
(hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
Full source 
theorem preimage_closedBall (hf : Isometry f) (x : α) (r : ℝ) :
    f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r :=
  hf.preimage_setOf_dist x (· ≤ r)
Isometry Preserves Closed Balls: $f^{-1}(\overline{B}(f(x), r)) = \overline{B}(x, r)$
Informal description
Let $f : \alpha \to \beta$ be an isometry between pseudometric spaces, and let $x \in \alpha$, $r \in \mathbb{R}$. Then the preimage under $f$ of the closed ball $\overline{B}(f(x), r)$ in $\beta$ is equal to the closed ball $\overline{B}(x, r)$ in $\alpha$, i.e., $$ f^{-1}(\overline{B}(f(x), r)) = \overline{B}(x, r). $$
Isometry.preimage_ball theorem
(hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.ball (f x) r = Metric.ball x r
Full source 
theorem preimage_ball (hf : Isometry f) (x : α) (r : ℝ) :
    f ⁻¹' Metric.ball (f x) r = Metric.ball x r :=
  hf.preimage_setOf_dist x (· < r)
Isometry Preserves Open Ball Preimages: $f^{-1}(\mathrm{ball}(f(x), r)) = \mathrm{ball}(x, r)$
Informal description
Let $f : \alpha \to \beta$ be an isometry between pseudometric spaces, and let $x \in \alpha$, $r \in \mathbb{R}$. Then the preimage under $f$ of the open ball $\mathrm{ball}(f(x), r)$ in $\beta$ is equal to the open ball $\mathrm{ball}(x, r)$ in $\alpha$, i.e., $$ f^{-1}(\mathrm{ball}(f(x), r)) = \mathrm{ball}(x, r). $$
Isometry.preimage_sphere theorem
(hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
Full source 
theorem preimage_sphere (hf : Isometry f) (x : α) (r : ℝ) :
    f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r :=
  hf.preimage_setOf_dist x (· = r)
Isometry Preserves Sphere Preimages: $f^{-1}(S(f(x), r)) = S(x, r)$
Informal description
Let $f : \alpha \to \beta$ be an isometry between pseudometric spaces, $x \in \alpha$, and $r \in \mathbb{R}$. Then the preimage under $f$ of the sphere centered at $f(x)$ with radius $r$ is equal to the sphere centered at $x$ with radius $r$, i.e., $$ f^{-1}(\{y \in \beta \mid \text{dist}(y, f(x)) = r\}) = \{y \in \alpha \mid \text{dist}(y, x) = r\}. $$
Isometry.mapsTo_ball theorem
(hf : Isometry f) (x : α) (r : ℝ) : MapsTo f (Metric.ball x r) (Metric.ball (f x) r)
Full source 
theorem mapsTo_ball (hf : Isometry f) (x : α) (r : ℝ) :
    MapsTo f (Metric.ball x r) (Metric.ball (f x) r) :=
  (hf.preimage_ball x r).ge
Isometry Maps Open Balls into Open Balls
Informal description
Let $f : \alpha \to \beta$ be an isometry between pseudometric spaces, and let $x \in \alpha$, $r \in \mathbb{R}$. Then $f$ maps the open ball $\mathrm{ball}(x, r)$ in $\alpha$ into the open ball $\mathrm{ball}(f(x), r)$ in $\beta$, i.e., $$ f(\mathrm{ball}(x, r)) \subseteq \mathrm{ball}(f(x), r). $$
Isometry.mapsTo_sphere theorem
(hf : Isometry f) (x : α) (r : ℝ) : MapsTo f (Metric.sphere x r) (Metric.sphere (f x) r)
Full source 
theorem mapsTo_sphere (hf : Isometry f) (x : α) (r : ℝ) :
    MapsTo f (Metric.sphere x r) (Metric.sphere (f x) r) :=
  (hf.preimage_sphere x r).ge
Isometry Maps Spheres to Spheres: $f(S(x, r)) \subseteq S(f(x), r)$
Informal description
Let $f : \alpha \to \beta$ be an isometry between pseudometric spaces, $x \in \alpha$, and $r \in \mathbb{R}$. Then $f$ maps the sphere centered at $x$ with radius $r$ into the sphere centered at $f(x)$ with radius $r$, i.e., $$ f(\{y \in \alpha \mid \text{dist}(y, x) = r\}) \subseteq \{y \in \beta \mid \text{dist}(y, f(x)) = r\}. $$
Isometry.mapsTo_closedBall theorem
(hf : Isometry f) (x : α) (r : ℝ) : MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) r)
Full source 
theorem mapsTo_closedBall (hf : Isometry f) (x : α) (r : ℝ) :
    MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) r) :=
  (hf.preimage_closedBall x r).ge
Isometry Maps Closed Balls into Closed Balls
Informal description
Let $f : \alpha \to \beta$ be an isometry between pseudometric spaces, $x \in \alpha$, and $r \in \mathbb{R}$. Then $f$ maps the closed ball $\overline{B}(x, r)$ in $\alpha$ into the closed ball $\overline{B}(f(x), r)$ in $\beta$, i.e., $$ f(\overline{B}(x, r)) \subseteq \overline{B}(f(x), r). $$
IsUniformEmbedding.to_isometry theorem
{α β} [UniformSpace α] [MetricSpace β] {f : α → β} (h : IsUniformEmbedding f) : (letI := h.comapMetricSpace f; Isometry f)
Full source 
/-- A uniform embedding from a uniform space to a metric space is an isometry with respect to the
induced metric space structure on the source space. -/
theorem IsUniformEmbedding.to_isometry {α β} [UniformSpace α] [MetricSpace β] {f : α → β}
    (h : IsUniformEmbedding f) : (letI := h.comapMetricSpace f; Isometry f) :=
  let _ := h.comapMetricSpace f
  Isometry.of_dist_eq fun _ _ => rfl
Uniform Embedding Induces Isometry via Pullback Metric
Informal description
Let $\alpha$ be a uniform space and $\beta$ a metric space. Given a uniformly embedding map $f \colon \alpha \to \beta$, when $\alpha$ is equipped with the metric space structure induced by $f$, the map $f$ becomes an isometry. That is, for any $x, y \in \alpha$, the distance between $f(x)$ and $f(y)$ in $\beta$ equals the distance between $x$ and $y$ in the induced metric on $\alpha$.
Topology.IsEmbedding.to_isometry theorem
{α β} [TopologicalSpace α] [MetricSpace β] {f : α → β} (h : IsEmbedding f) : (letI := h.comapMetricSpace f; Isometry f)
Full source 
/-- An embedding from a topological space to a metric space is an isometry with respect to the
induced metric space structure on the source space. -/
theorem Topology.IsEmbedding.to_isometry {α β} [TopologicalSpace α] [MetricSpace β] {f : α → β}
    (h : IsEmbedding f) : (letI := h.comapMetricSpace f; Isometry f) :=
  let _ := h.comapMetricSpace f
  Isometry.of_dist_eq fun _ _ => rfl
Topological Embedding Induces Isometry via Pullback Metric
Informal description
Let $\alpha$ be a topological space and $\beta$ a metric space. Given a topological embedding $f \colon \alpha \to \beta$, when $\alpha$ is equipped with the metric space structure induced by $f$ (where the distance between $x, y \in \alpha$ is defined as $\text{dist}(f(x), f(y))$), the map $f$ becomes an isometry. That is, $f$ preserves distances under this induced metric.
PseudoEMetricSpace.isometry_induced theorem
(f : α → β) [m : PseudoEMetricSpace β] : letI := m.induced f; Isometry f
Full source 
theorem PseudoEMetricSpace.isometry_induced (f : α → β) [m : PseudoEMetricSpace β] :
    letI := m.induced f; Isometry f := fun _ _ ↦ rfl
Induced Pseudoemetric Structure Makes $f$ an Isometry
Informal description
Let $f : \alpha \to \beta$ be a function between types, where $\beta$ is equipped with a pseudoemetric space structure. When $\alpha$ is given the induced pseudoemetric space structure from $f$, then $f$ becomes an isometry. That is, for any $x_1, x_2 \in \alpha$, the distance between $f(x_1)$ and $f(x_2)$ in $\beta$ equals the distance between $x_1$ and $x_2$ in the induced structure on $\alpha$.
PsuedoMetricSpace.isometry_induced theorem
(f : α → β) [m : PseudoMetricSpace β] : letI := m.induced f; Isometry f
Full source 
theorem PsuedoMetricSpace.isometry_induced (f : α → β) [m : PseudoMetricSpace β] :
    letI := m.induced f; Isometry f := fun _ _ ↦ rfl
Induced Pseudometric Structure Makes $f$ an Isometry
Informal description
Let $f : \alpha \to \beta$ be a function between types, where $\beta$ is equipped with a pseudometric space structure. When $\alpha$ is given the induced pseudometric space structure from $f$, then $f$ becomes an isometry. That is, for any $x_1, x_2 \in \alpha$, the distance between $f(x_1)$ and $f(x_2)$ in $\beta$ equals the distance between $x_1$ and $x_2$ in the induced structure on $\alpha$.
EMetricSpace.isometry_induced theorem
(f : α → β) (hf : f.Injective) [m : EMetricSpace β] : letI := m.induced f hf; Isometry f
Full source 
theorem EMetricSpace.isometry_induced (f : α → β) (hf : f.Injective) [m : EMetricSpace β] :
    letI := m.induced f hf; Isometry f := fun _ _ ↦ rfl
Injective Function Induces Isometry on Induced EMetric Space
Informal description
Let $f : \alpha \to \beta$ be an injective function from a type $\alpha$ to an emetric space $\beta$. When $\alpha$ is equipped with the emetric space structure induced by $f$, then $f$ becomes an isometry. That is, for any $x_1, x_2 \in \alpha$, the distance between $f(x_1)$ and $f(x_2)$ in $\beta$ equals the distance between $x_1$ and $x_2$ in the induced emetric space structure on $\alpha$.
MetricSpace.isometry_induced theorem
(f : α → β) (hf : f.Injective) [m : MetricSpace β] : letI := m.induced f hf; Isometry f
Full source 
theorem MetricSpace.isometry_induced (f : α → β) (hf : f.Injective) [m : MetricSpace β] :
    letI := m.induced f hf; Isometry f := fun _ _ ↦ rfl
Injective Function Induces Isometry on Induced Metric Space
Informal description
Let $f \colon \alpha \to \beta$ be an injective function from a type $\alpha$ to a metric space $\beta$. When $\alpha$ is equipped with the metric space structure induced by $f$, then $f$ becomes an isometry. That is, for any $x_1, x_2 \in \alpha$, the distance between $f(x_1)$ and $f(x_2)$ in $\beta$ equals the distance between $x_1$ and $x_2$ in the induced metric space structure on $\alpha$.
IsometryEquiv structure
(α : Type u) (β : Type v) [PseudoEMetricSpace α] [PseudoEMetricSpace β] extends α ≃ β
Full source 
/-- `α` and `β` are isometric if there is an isometric bijection between them. -/
structure IsometryEquiv (α : Type u) (β : Type v) [PseudoEMetricSpace α] [PseudoEMetricSpace β]
    extends α ≃ β where
  isometry_toFun : Isometry toFun
Isometric Equivalence
Informal description
An isometric equivalence between two pseudo-emetric spaces $\alpha$ and $\beta$ is a bijection $f : \alpha \to \beta$ that preserves the edistance, i.e., for all $x, y \in \alpha$, the edistance between $f(x)$ and $f(y)$ equals the edistance between $x$ and $y$.
term_≃ᵢ_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc]
infixl:25 " ≃ᵢ " => IsometryEquiv
Isometric equivalence notation
Informal description
The notation `≃ᵢ` represents an isometric equivalence between two pseudo-emetric spaces, i.e., a bijective isometry between the spaces.
IsometryEquiv.toEquiv_injective theorem
: Injective (toEquiv : (α ≃ᵢ β) → (α ≃ β))
Full source 
theorem toEquiv_injective : Injective (toEquiv : (α ≃ᵢ β) → (α ≃ β))
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
Injectivity of the Underlying Bijection Map for Isometric Equivalences
Informal description
The map that sends an isometric equivalence $e : \alpha \simeqᵢ \beta$ between pseudo-emetric spaces to its underlying bijection $e.toEquiv : \alpha \simeq \beta$ is injective. In other words, if two isometric equivalences have the same underlying bijection, then they are equal.
IsometryEquiv.toEquiv_inj theorem
{e₁ e₂ : α ≃ᵢ β} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
Full source 
@[simp] theorem toEquiv_inj {e₁ e₂ : α ≃ᵢ β} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂ :=
  toEquiv_injective.eq_iff
Equality of Isometric Equivalences via Underlying Bijections
Informal description
For any two isometric equivalences $e_1, e_2$ between pseudo-emetric spaces $\alpha$ and $\beta$, the underlying bijections of $e_1$ and $e_2$ are equal if and only if $e_1$ and $e_2$ are equal as isometric equivalences. In other words, $e_1.\text{toEquiv} = e_2.\text{toEquiv} \leftrightarrow e_1 = e_2$.
IsometryEquiv.instEquivLike instance
: EquivLike (α ≃ᵢ β) α β
Full source 
instance : EquivLike (α ≃ᵢ β) α β where
  coe e := e.toEquiv
  inv e := e.toEquiv.symm
  left_inv e := e.left_inv
  right_inv e := e.right_inv
  coe_injective' _ _ h _ := toEquiv_injective <| DFunLike.ext' h
Isometric Equivalence as Function-Like Object
Informal description
For any two pseudo-emetric spaces $\alpha$ and $\beta$, an isometric equivalence $\alpha \simeq \beta$ can be treated as a function-like object from $\alpha$ to $\beta$.
IsometryEquiv.coe_eq_toEquiv theorem
(h : α ≃ᵢ β) (a : α) : h a = h.toEquiv a
Full source 
theorem coe_eq_toEquiv (h : α ≃ᵢ β) (a : α) : h a = h.toEquiv a := rfl
Isometric Equivalence Application Equals Underlying Bijection Application
Informal description
For any isometric equivalence $h$ between pseudo-emetric spaces $\alpha$ and $\beta$, and for any element $a \in \alpha$, the application of $h$ to $a$ is equal to the application of the underlying bijection $h.\text{toEquiv}$ to $a$, i.e., $h(a) = h.\text{toEquiv}(a)$.
IsometryEquiv.coe_toEquiv theorem
(h : α ≃ᵢ β) : ⇑h.toEquiv = h
Full source 
@[simp] theorem coe_toEquiv (h : α ≃ᵢ β) : ⇑h.toEquiv = h := rfl
Underlying Function of Isometric Equivalence Matches the Equivalence
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between two pseudo-emetric spaces $\alpha$ and $\beta$, the underlying function of the equivalence $h.\text{toEquiv}$ is equal to $h$ itself.
IsometryEquiv.coe_mk theorem
(e : α ≃ β) (h) : ⇑(mk e h) = e
Full source 
@[simp] theorem coe_mk (e : α ≃ β) (h) : ⇑(mk e h) = e := rfl
Underlying Function of Isometric Equivalence Construction
Informal description
For any bijection $e : \alpha \simeq \beta$ and any proof $h$ that $e$ is an isometry, the underlying function of the constructed isometric equivalence $\alpha \simeqᵢ \beta$ is equal to $e$.
IsometryEquiv.isometry theorem
(h : α ≃ᵢ β) : Isometry h
Full source 
protected theorem isometry (h : α ≃ᵢ β) : Isometry h :=
  h.isometry_toFun
Isometric Equivalence Preserves Distance
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between two pseudoemetric spaces $\alpha$ and $\beta$, the map $h$ is an isometry, i.e., it preserves the extended distance between points.
IsometryEquiv.bijective theorem
(h : α ≃ᵢ β) : Bijective h
Full source 
protected theorem bijective (h : α ≃ᵢ β) : Bijective h :=
  h.toEquiv.bijective
Bijectivity of Isometric Equivalences
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between two pseudo-emetric spaces $\alpha$ and $\beta$, the function $h$ is bijective. That is, $h$ is both injective (for any $x, y \in \alpha$, $h(x) = h(y)$ implies $x = y$) and surjective (for every $y \in \beta$, there exists an $x \in \alpha$ such that $h(x) = y$).
IsometryEquiv.injective theorem
(h : α ≃ᵢ β) : Injective h
Full source 
protected theorem injective (h : α ≃ᵢ β) : Injective h :=
  h.toEquiv.injective
Injectivity of Isometric Equivalences
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between two pseudo-emetric spaces $\alpha$ and $\beta$, the function $h$ is injective. That is, for any $x, y \in \alpha$, if $h(x) = h(y)$, then $x = y$.
IsometryEquiv.surjective theorem
(h : α ≃ᵢ β) : Surjective h
Full source 
protected theorem surjective (h : α ≃ᵢ β) : Surjective h :=
  h.toEquiv.surjective
Surjectivity of Isometric Equivalences
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between two pseudo-emetric spaces $\alpha$ and $\beta$, the function $h$ is surjective. That is, for every $y \in \beta$, there exists an $x \in \alpha$ such that $h(x) = y$.
IsometryEquiv.edist_eq theorem
(h : α ≃ᵢ β) (x y : α) : edist (h x) (h y) = edist x y
Full source 
protected theorem edist_eq (h : α ≃ᵢ β) (x y : α) : edist (h x) (h y) = edist x y :=
  h.isometry.edist_eq x y
Isometric Equivalence Preserves Extended Distance
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between two pseudoemetric spaces $\alpha$ and $\beta$, and for any two points $x, y \in \alpha$, the extended distance between $h(x)$ and $h(y)$ in $\beta$ is equal to the extended distance between $x$ and $y$ in $\alpha$, i.e., \[ \text{edist}(h(x), h(y)) = \text{edist}(x, y). \]
IsometryEquiv.dist_eq theorem
{α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x y : α) : dist (h x) (h y) = dist x y
Full source 
protected theorem dist_eq {α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β)
    (x y : α) : dist (h x) (h y) = dist x y :=
  h.isometry.dist_eq x y
Isometric Equivalence Preserves Distance
Informal description
Let $\alpha$ and $\beta$ be pseudometric spaces, and let $h \colon \alpha \simeq \beta$ be an isometric equivalence between them. Then for any two points $x, y \in \alpha$, the distance between $h(x)$ and $h(y)$ in $\beta$ equals the distance between $x$ and $y$ in $\alpha$, i.e., \[ \text{dist}(h(x), h(y)) = \text{dist}(x, y). \]
IsometryEquiv.nndist_eq theorem
{α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x y : α) : nndist (h x) (h y) = nndist x y
Full source 
protected theorem nndist_eq {α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β)
    (x y : α) : nndist (h x) (h y) = nndist x y :=
  h.isometry.nndist_eq x y
Isometric Equivalence Preserves Non-Negative Distance
Informal description
For any two pseudometric spaces $\alpha$ and $\beta$, and any isometric equivalence $h \colon \alpha \simeq \beta$, the non-negative distance between $h(x)$ and $h(y)$ in $\beta$ equals the non-negative distance between $x$ and $y$ in $\alpha$, i.e., \[ \text{nndist}(h(x), h(y)) = \text{nndist}(x, y). \]
IsometryEquiv.continuous theorem
(h : α ≃ᵢ β) : Continuous h
Full source 
protected theorem continuous (h : α ≃ᵢ β) : Continuous h :=
  h.isometry.continuous
Continuity of Isometric Equivalences
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between pseudo-metric spaces $\alpha$ and $\beta$, the map $h$ is continuous.
IsometryEquiv.ediam_image theorem
(h : α ≃ᵢ β) (s : Set α) : EMetric.diam (h '' s) = EMetric.diam s
Full source 
@[simp]
theorem ediam_image (h : α ≃ᵢ β) (s : Set α) : EMetric.diam (h '' s) = EMetric.diam s :=
  h.isometry.ediam_image s
Isometric Equivalence Preserves Extended Diameter of Subsets
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudo-emetric spaces $\alpha$ and $\beta$, and any subset $s \subseteq \alpha$, the extended diameter of the image $h(s)$ in $\beta$ equals the extended diameter of $s$ in $\alpha$, i.e., \[ \text{diam}(h(s)) = \text{diam}(s). \]
IsometryEquiv.ext theorem
⦃h₁ h₂ : α ≃ᵢ β⦄ (H : ∀ x, h₁ x = h₂ x) : h₁ = h₂
Full source 
@[ext]
theorem ext ⦃h₁ h₂ : α ≃ᵢ β⦄ (H : ∀ x, h₁ x = h₂ x) : h₁ = h₂ :=
  DFunLike.ext _ _ H
Extensionality of Isometric Equivalences
Informal description
For any two isometric equivalences $h₁, h₂ : \alpha \simeq \beta$ between pseudo-emetric spaces $\alpha$ and $\beta$, if $h₁(x) = h₂(x)$ for all $x \in \alpha$, then $h₁ = h₂$.
IsometryEquiv.mk' definition
{α : Type u} [EMetricSpace α] (f : α → β) (g : β → α) (hfg : ∀ x, f (g x) = x) (hf : Isometry f) : α ≃ᵢ β
Full source 
/-- Alternative constructor for isometric bijections,
taking as input an isometry, and a right inverse. -/
def mk' {α : Type u} [EMetricSpace α] (f : α → β) (g : β → α) (hfg : ∀ x, f (g x) = x)
    (hf : Isometry f) : α ≃ᵢ β where
  toFun := f
  invFun := g
  left_inv _ := hf.injective <| hfg _
  right_inv := hfg
  isometry_toFun := hf
Isometric equivalence from isometry with right inverse
Informal description
Given an emetric space $\alpha$ and a function $f: \alpha \to \beta$ with a right inverse $g: \beta \to \alpha$ (i.e., $f(g(x)) = x$ for all $x \in \beta$), if $f$ is an isometry, then $f$ induces an isometric equivalence between $\alpha$ and $\beta$.
IsometryEquiv.refl definition
(α : Type*) [PseudoEMetricSpace α] : α ≃ᵢ α
Full source 
/-- The identity isometry of a space. -/
protected def refl (α : Type*) [PseudoEMetricSpace α] : α ≃ᵢ α :=
  { Equiv.refl α with isometry_toFun := isometry_id }
Identity isometric equivalence
Informal description
The identity isometric equivalence on a pseudo-emetric space $\alpha$, which is the bijection from $\alpha$ to itself given by the identity function, preserving the extended distance between any two points.
IsometryEquiv.trans definition
(h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) : α ≃ᵢ γ
Full source 
/-- The composition of two isometric isomorphisms, as an isometric isomorphism. -/
protected def trans (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) : α ≃ᵢ γ :=
  { Equiv.trans h₁.toEquiv h₂.toEquiv with
    isometry_toFun := h₂.isometry_toFun.comp h₁.isometry_toFun }
Composition of isometric equivalences
Informal description
Given two isometric equivalences $h₁ : \alpha \simeq \beta$ and $h₂ : \beta \simeq \gamma$ between pseudo-emetric spaces, their composition $h₂ \circ h₁$ forms an isometric equivalence $\alpha \simeq \gamma$, where the distance-preserving property is inherited from both $h₁$ and $h₂$.
IsometryEquiv.trans_apply theorem
(h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : α) : h₁.trans h₂ x = h₂ (h₁ x)
Full source 
@[simp]
theorem trans_apply (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : α) : h₁.trans h₂ x = h₂ (h₁ x) :=
  rfl
Composition of Isometric Equivalences Evaluated at a Point: $(h₁ \circ h₂)(x) = h₂(h₁(x))$
Informal description
For any isometric equivalences $h₁ : \alpha \simeq \beta$ and $h₂ : \beta \simeq \gamma$ between pseudo-emetric spaces, and for any point $x \in \alpha$, the composition $h₁ \circ h₂$ evaluated at $x$ equals $h₂(h₁(x))$.
IsometryEquiv.symm definition
(h : α ≃ᵢ β) : β ≃ᵢ α
Full source 
/-- The inverse of an isometric isomorphism, as an isometric isomorphism. -/
protected def symm (h : α ≃ᵢ β) : β ≃ᵢ α where
  isometry_toFun := h.isometry.right_inv h.right_inv
  toEquiv := h.toEquiv.symm
Inverse of an isometric equivalence
Informal description
Given an isometric equivalence $h : \alpha \simeq \beta$ between two pseudo-emetric spaces, the inverse $h^{-1} : \beta \simeq \alpha$ is also an isometric equivalence. This means that $h^{-1}$ preserves the edistance, i.e., for all $x, y \in \beta$, the edistance between $h^{-1}(x)$ and $h^{-1}(y)$ equals the edistance between $x$ and $y$.
IsometryEquiv.Simps.apply definition
(h : α ≃ᵢ β) : α → β
Full source 
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def Simps.apply (h : α ≃ᵢ β) : α → β := h
Application of an isometric equivalence
Informal description
The function that maps an element \( x \) of a pseudo-emetric space \( \alpha \) to its image under the isometric equivalence \( h : \alpha \simeq \beta \).
IsometryEquiv.Simps.symm_apply definition
(h : α ≃ᵢ β) : β → α
Full source 
/-- See Note [custom simps projection] -/
def Simps.symm_apply (h : α ≃ᵢ β) : β → α :=
  h.symm
Inverse map of an isometric equivalence
Informal description
For an isometric equivalence $h : \alpha \simeq \beta$ between two pseudo-emetric spaces, the function maps an element $y \in \beta$ to its preimage $h^{-1}(y) \in \alpha$ under the isometric equivalence.
IsometryEquiv.symm_symm theorem
(h : α ≃ᵢ β) : h.symm.symm = h
Full source 
@[simp]
theorem symm_symm (h : α ≃ᵢ β) : h.symm.symm = h := rfl
Double Inverse of Isometric Equivalence
Informal description
For any isometric equivalence $h$ between two pseudo-emetric spaces $\alpha$ and $\beta$, the inverse of the inverse of $h$ is equal to $h$ itself, i.e., $(h^{-1})^{-1} = h$.
IsometryEquiv.symm_bijective theorem
: Bijective (IsometryEquiv.symm : (α ≃ᵢ β) → β ≃ᵢ α)
Full source 
theorem symm_bijective : Bijective (IsometryEquiv.symm : (α ≃ᵢ β) → β ≃ᵢ α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
Bijectivity of the Inverse Map on Isometric Equivalences
Informal description
The inverse map $\text{symm} : (\alpha \simeqᵢ \beta) \to (\beta \simeqᵢ \alpha)$, which sends an isometric equivalence to its inverse, is bijective. That is, it is both injective (distinct isometric equivalences have distinct inverses) and surjective (every isometric equivalence from $\beta$ to $\alpha$ is the inverse of some isometric equivalence from $\alpha$ to $\beta$).
IsometryEquiv.apply_symm_apply theorem
(h : α ≃ᵢ β) (y : β) : h (h.symm y) = y
Full source 
@[simp]
theorem apply_symm_apply (h : α ≃ᵢ β) (y : β) : h (h.symm y) = y :=
  h.toEquiv.apply_symm_apply y
Recovery of Element via Isometric Equivalence: $h(h^{-1}(y)) = y$
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudo-emetric spaces and any element $y \in \beta$, applying $h$ to the inverse image $h^{-1}(y)$ recovers the original element $y$, i.e., $h(h^{-1}(y)) = y$.
IsometryEquiv.symm_apply_apply theorem
(h : α ≃ᵢ β) (x : α) : h.symm (h x) = x
Full source 
@[simp]
theorem symm_apply_apply (h : α ≃ᵢ β) (x : α) : h.symm (h x) = x :=
  h.toEquiv.symm_apply_apply x
Inverse Isometry Recovers Original Element
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between pseudo-emetric spaces and any element $x \in \alpha$, applying the inverse isometry $h^{-1}$ to the image $h(x)$ recovers the original element $x$, i.e., $h^{-1}(h(x)) = x$.
IsometryEquiv.symm_apply_eq theorem
(h : α ≃ᵢ β) {x : α} {y : β} : h.symm y = x ↔ y = h x
Full source 
theorem symm_apply_eq (h : α ≃ᵢ β) {x : α} {y : β} : h.symm y = x ↔ y = h x :=
  h.toEquiv.symm_apply_eq
Characterization of Inverse Isometry: $h^{-1}(y) = x \leftrightarrow y = h(x)$
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between pseudo-emetric spaces, and for any elements $x \in \alpha$ and $y \in \beta$, the equality $h^{-1}(y) = x$ holds if and only if $y = h(x)$.
IsometryEquiv.symm_comp_self theorem
(h : α ≃ᵢ β) : (h.symm : β → α) ∘ h = id
Full source 
theorem symm_comp_self (h : α ≃ᵢ β) : (h.symm : β → α) ∘ h = id := funext h.left_inv
Inverse Composition of Isometric Equivalence Yields Identity
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudo-emetric spaces, the composition of the inverse map $h^{-1} \colon \beta \to \alpha$ with $h$ is the identity function on $\alpha$, i.e., $h^{-1} \circ h = \text{id}_\alpha$.
IsometryEquiv.self_comp_symm theorem
(h : α ≃ᵢ β) : (h : α → β) ∘ h.symm = id
Full source 
theorem self_comp_symm (h : α ≃ᵢ β) : (h : α → β) ∘ h.symm = id := funext h.right_inv
Composition of Isometric Equivalence with its Inverse Yields Identity
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudo-emetric spaces, the composition of $h$ with its inverse $h^{-1}$ is the identity function on $\beta$, i.e., $h \circ h^{-1} = \text{id}_\beta$.
IsometryEquiv.range_eq_univ theorem
(h : α ≃ᵢ β) : range h = univ
Full source 
theorem range_eq_univ (h : α ≃ᵢ β) : range h = univ := by simp
Range of Isometric Equivalence is Universal Set
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between two pseudo-emetric spaces $\alpha$ and $\beta$, the range of $h$ is equal to the universal set of $\beta$. In other words, $h$ is surjective.
IsometryEquiv.image_symm theorem
(h : α ≃ᵢ β) : image h.symm = preimage h
Full source 
theorem image_symm (h : α ≃ᵢ β) : image h.symm = preimage h :=
  image_eq_preimage_of_inverse h.symm.toEquiv.left_inv h.symm.toEquiv.right_inv
Image of Inverse Equals Preimage for Isometric Equivalence
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudo-emetric spaces, the image of the inverse isometric equivalence $h^{-1}$ is equal to the preimage of $h$. In other words, for any subset $S \subseteq \alpha$, we have $h^{-1}(S) = h^{-1}(S)$ as sets in $\beta$.
IsometryEquiv.preimage_symm theorem
(h : α ≃ᵢ β) : preimage h.symm = image h
Full source 
theorem preimage_symm (h : α ≃ᵢ β) : preimage h.symm = image h :=
  (image_eq_preimage_of_inverse h.toEquiv.left_inv h.toEquiv.right_inv).symm
Preimage of Inverse Equals Image in Isometric Equivalence
Informal description
For any isometric equivalence $h : \alpha \simeq \beta$ between two pseudo-emetric spaces, the preimage of $h^{-1}$ is equal to the image of $h$. In other words, for any subset $s \subseteq \beta$, we have $h^{-1}(s) = h(s)$.
IsometryEquiv.symm_trans_apply theorem
(h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : γ) : (h₁.trans h₂).symm x = h₁.symm (h₂.symm x)
Full source 
@[simp]
theorem symm_trans_apply (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : γ) :
    (h₁.trans h₂).symm x = h₁.symm (h₂.symm x) :=
  rfl
Inverse of Composition of Isometric Equivalences
Informal description
For any isometric equivalences $h₁ : \alpha \simeq \beta$ and $h₂ : \beta \simeq \gamma$ between pseudo-emetric spaces, and for any point $x \in \gamma$, the inverse of the composition $(h₁ \circ h₂)^{-1}(x)$ equals the composition of the inverses $h₁^{-1}(h₂^{-1}(x))$.
IsometryEquiv.ediam_univ theorem
(h : α ≃ᵢ β) : EMetric.diam (univ : Set α) = EMetric.diam (univ : Set β)
Full source 
theorem ediam_univ (h : α ≃ᵢ β) : EMetric.diam (univ : Set α) = EMetric.diam (univ : Set β) := by
  rw [← h.range_eq_univ, h.isometry.ediam_range]
Isometric Equivalence Preserves Extended Diameter of Universal Sets
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudoemetric spaces $\alpha$ and $\beta$, the extended diameter of the universal set in $\alpha$ is equal to the extended diameter of the universal set in $\beta$, i.e., \[ \text{diam}(\text{univ} \subseteq \alpha) = \text{diam}(\text{univ} \subseteq \beta). \]
IsometryEquiv.ediam_preimage theorem
(h : α ≃ᵢ β) (s : Set β) : EMetric.diam (h ⁻¹' s) = EMetric.diam s
Full source 
@[simp]
theorem ediam_preimage (h : α ≃ᵢ β) (s : Set β) : EMetric.diam (h ⁻¹' s) = EMetric.diam s := by
  rw [← image_symm, ediam_image]
Isometric Equivalence Preserves Extended Diameter of Preimages
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudo-emetric spaces and any subset $s \subseteq \beta$, the extended diameter of the preimage $h^{-1}(s)$ in $\alpha$ equals the extended diameter of $s$ in $\beta$, i.e., \[ \text{diam}(h^{-1}(s)) = \text{diam}(s). \]
IsometryEquiv.preimage_emetric_ball theorem
(h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) : h ⁻¹' EMetric.ball x r = EMetric.ball (h.symm x) r
Full source 
@[simp]
theorem preimage_emetric_ball (h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) :
    h ⁻¹' EMetric.ball x r = EMetric.ball (h.symm x) r := by
  rw [← h.isometry.preimage_emetric_ball (h.symm x) r, h.apply_symm_apply]
Preimage of Open Ball under Isometric Equivalence
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudoemetric spaces $\alpha$ and $\beta$. For any point $x \in \beta$ and any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage under $h$ of the open ball $B(x, r) \subseteq \beta$ is equal to the open ball $B(h^{-1}(x), r) \subseteq \alpha$. In other words, \[ h^{-1}\big(B(x, r)\big) = B(h^{-1}(x), r). \]
IsometryEquiv.preimage_emetric_closedBall theorem
(h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) : h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (h.symm x) r
Full source 
@[simp]
theorem preimage_emetric_closedBall (h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) :
    h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (h.symm x) r := by
  rw [← h.isometry.preimage_emetric_closedBall (h.symm x) r, h.apply_symm_apply]
Preimage of Closed Ball under Isometric Equivalence
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudoemetric spaces $\alpha$ and $\beta$. For any point $x \in \beta$ and any extended nonnegative real number $r \in [0, \infty]$, the preimage under $h$ of the closed ball $\overline{B}(x, r)$ in $\beta$ is equal to the closed ball $\overline{B}(h^{-1}(x), r)$ in $\alpha$. That is, \[ h^{-1}(\overline{B}(x, r)) = \overline{B}(h^{-1}(x), r). \]
IsometryEquiv.image_emetric_ball theorem
(h : α ≃ᵢ β) (x : α) (r : ℝ≥0∞) : h '' EMetric.ball x r = EMetric.ball (h x) r
Full source 
@[simp]
theorem image_emetric_ball (h : α ≃ᵢ β) (x : α) (r : ℝ≥0∞) :
    h '' EMetric.ball x r = EMetric.ball (h x) r := by
  rw [← h.preimage_symm, h.symm.preimage_emetric_ball, symm_symm]
Image of Open Ball under Isometric Equivalence
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudoemetric spaces $\alpha$ and $\beta$. For any point $x \in \alpha$ and any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the image under $h$ of the open ball $B(x, r) \subseteq \alpha$ is equal to the open ball $B(h(x), r) \subseteq \beta$. In other words, \[ h\big(B(x, r)\big) = B(h(x), r). \]
IsometryEquiv.image_emetric_closedBall theorem
(h : α ≃ᵢ β) (x : α) (r : ℝ≥0∞) : h '' EMetric.closedBall x r = EMetric.closedBall (h x) r
Full source 
@[simp]
theorem image_emetric_closedBall (h : α ≃ᵢ β) (x : α) (r : ℝ≥0∞) :
    h '' EMetric.closedBall x r = EMetric.closedBall (h x) r := by
  rw [← h.preimage_symm, h.symm.preimage_emetric_closedBall, symm_symm]
Image of Closed Ball under Isometric Equivalence
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudoemetric spaces $\alpha$ and $\beta$. For any point $x \in \alpha$ and any extended nonnegative real number $r \in [0, \infty]$, the image under $h$ of the closed ball $\overline{B}(x, r)$ in $\alpha$ is equal to the closed ball $\overline{B}(h(x), r)$ in $\beta$. That is, \[ h(\overline{B}(x, r)) = \overline{B}(h(x), r). \]
IsometryEquiv.toHomeomorph definition
(h : α ≃ᵢ β) : α ≃ₜ β
Full source 
/-- The (bundled) homeomorphism associated to an isometric isomorphism. -/
@[simps toEquiv]
protected def toHomeomorph (h : α ≃ᵢ β) : α ≃ₜ β where
  continuous_toFun := h.continuous
  continuous_invFun := h.symm.continuous
  toEquiv := h.toEquiv
Homeomorphism induced by an isometric equivalence
Informal description
Given an isometric equivalence $h \colon \alpha \simeq \beta$ between pseudo-emetric spaces $\alpha$ and $\beta$, the function `IsometryEquiv.toHomeomorph` constructs a homeomorphism (a continuous bijection with continuous inverse) between $\alpha$ and $\beta$ by using $h$ as the underlying bijection. The continuity of both $h$ and its inverse $h^{-1}$ is ensured by the isometric property of $h$.
IsometryEquiv.coe_toHomeomorph theorem
(h : α ≃ᵢ β) : ⇑h.toHomeomorph = h
Full source 
@[simp]
theorem coe_toHomeomorph (h : α ≃ᵢ β) : ⇑h.toHomeomorph = h :=
  rfl
Homeomorphism Function from Isometric Equivalence Equals Original Isometry
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between pseudo-emetric spaces $\alpha$ and $\beta$, the underlying function of the homeomorphism induced by $h$ is equal to $h$ itself. That is, $h_{\text{toHomeomorph}} = h$.
IsometryEquiv.coe_toHomeomorph_symm theorem
(h : α ≃ᵢ β) : ⇑h.toHomeomorph.symm = h.symm
Full source 
@[simp]
theorem coe_toHomeomorph_symm (h : α ≃ᵢ β) : ⇑h.toHomeomorph.symm = h.symm :=
  rfl
Inverse Homeomorphism of Isometric Equivalence Equals Inverse Isometry
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between pseudo-emetric spaces $\alpha$ and $\beta$, the underlying function of the inverse homeomorphism $h^{-1}$ equals the underlying function of the inverse isometric equivalence $h^{-1}$.
IsometryEquiv.comp_continuousOn_iff theorem
{γ} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α} {s : Set γ} : ContinuousOn (h ∘ f) s ↔ ContinuousOn f s
Full source 
@[simp]
theorem comp_continuousOn_iff {γ} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α} {s : Set γ} :
    ContinuousOnContinuousOn (h ∘ f) s ↔ ContinuousOn f s :=
  h.toHomeomorph.comp_continuousOn_iff _ _
Continuity of Composition with Isometric Equivalence on a Subset
Informal description
Let $\alpha$ and $\beta$ be pseudo-emetric spaces, and let $h \colon \alpha \simeq \beta$ be an isometric equivalence. For any topological space $\gamma$, a function $f \colon \gamma \to \alpha$, and a subset $s \subseteq \gamma$, the composition $h \circ f$ is continuous on $s$ if and only if $f$ is continuous on $s$.
IsometryEquiv.comp_continuous_iff theorem
{γ} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α} : Continuous (h ∘ f) ↔ Continuous f
Full source 
@[simp]
theorem comp_continuous_iff {γ} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α} :
    ContinuousContinuous (h ∘ f) ↔ Continuous f :=
  h.toHomeomorph.comp_continuous_iff
Continuity of Composition with Isometric Equivalence
Informal description
Let $\alpha$ and $\beta$ be pseudo-emetric spaces, and let $h \colon \alpha \simeq \beta$ be an isometric equivalence. For any topological space $\gamma$ and any function $f \colon \gamma \to \alpha$, the composition $h \circ f$ is continuous if and only if $f$ is continuous.
IsometryEquiv.comp_continuous_iff' theorem
{γ} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : β → γ} : Continuous (f ∘ h) ↔ Continuous f
Full source 
@[simp]
theorem comp_continuous_iff' {γ} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : β → γ} :
    ContinuousContinuous (f ∘ h) ↔ Continuous f :=
  h.toHomeomorph.comp_continuous_iff'
Continuity of Composition with Isometric Equivalence
Informal description
Let $\alpha$ and $\beta$ be pseudo-emetric spaces, and let $h \colon \alpha \simeq \beta$ be an isometric equivalence. For any topological space $\gamma$ and any function $f \colon \beta \to \gamma$, the composition $f \circ h$ is continuous if and only if $f$ is continuous.
IsometryEquiv.instGroup instance
: Group (α ≃ᵢ α)
Full source 
/-- The group of isometries. -/
instance : Group (α ≃ᵢ α) where
  one := IsometryEquiv.refl _
  mul e₁ e₂ := e₂.trans e₁
  inv := IsometryEquiv.symm
  mul_assoc _ _ _ := rfl
  one_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl
  inv_mul_cancel e := ext e.symm_apply_apply
Group Structure on Isometric Self-Equivalences
Informal description
For any pseudo-emetric space $\alpha$, the set of isometric self-equivalences $\alpha \simeq \alpha$ forms a group under composition. The group operation is given by composition of isometries, the identity element is the identity isometry, and the inverse of an isometry is its inverse function.
IsometryEquiv.coe_one theorem
: ⇑(1 : α ≃ᵢ α) = id
Full source 
@[simp] theorem coe_one : ⇑(1 : α ≃ᵢ α) = id := rfl
Identity Isometry as Identity Function
Informal description
The identity isometric equivalence on a pseudo-emetric space $\alpha$ corresponds to the identity function, i.e., the coercion of the multiplicative identity element in the group of isometric self-equivalences of $\alpha$ is equal to the identity map $\text{id}$.
IsometryEquiv.coe_mul theorem
(e₁ e₂ : α ≃ᵢ α) : ⇑(e₁ * e₂) = e₁ ∘ e₂
Full source 
@[simp] theorem coe_mul (e₁ e₂ : α ≃ᵢ α) : ⇑(e₁ * e₂) = e₁ ∘ e₂ := rfl
Composition of Isometric Self-Equivalences Preserves Function Composition
Informal description
For any two isometric self-equivalences $e₁$ and $e₂$ on a pseudo-emetric space $\alpha$, the underlying function of their composition $e₁ * e₂$ is equal to the composition of their underlying functions, i.e., $(e₁ * e₂)(x) = e₁(e₂(x))$ for all $x \in \alpha$.
IsometryEquiv.mul_apply theorem
(e₁ e₂ : α ≃ᵢ α) (x : α) : (e₁ * e₂) x = e₁ (e₂ x)
Full source 
theorem mul_apply (e₁ e₂ : α ≃ᵢ α) (x : α) : (e₁ * e₂) x = e₁ (e₂ x) := rfl
Composition of Isometric Self-Equivalences Evaluated at a Point
Informal description
Let $\alpha$ be a pseudo-emetric space. For any two isometric self-equivalences $e_1, e_2 : \alpha \simeq \alpha$ and any point $x \in \alpha$, the composition $e_1 \circ e_2$ evaluated at $x$ equals $e_1$ evaluated at $e_2(x)$, i.e., $(e_1 \circ e_2)(x) = e_1(e_2(x))$.
IsometryEquiv.inv_apply_self theorem
(e : α ≃ᵢ α) (x : α) : e⁻¹ (e x) = x
Full source 
@[simp] theorem inv_apply_self (e : α ≃ᵢ α) (x : α) : e⁻¹ (e x) = x := e.symm_apply_apply x
Inverse Isometry Recovers Original Element
Informal description
For any isometric self-equivalence $e$ of a pseudo-emetric space $\alpha$ and any element $x \in \alpha$, applying the inverse isometry $e^{-1}$ to the image $e(x)$ recovers the original element $x$, i.e., $e^{-1}(e(x)) = x$.
IsometryEquiv.apply_inv_self theorem
(e : α ≃ᵢ α) (x : α) : e (e⁻¹ x) = x
Full source 
@[simp] theorem apply_inv_self (e : α ≃ᵢ α) (x : α) : e (e⁻¹ x) = x := e.apply_symm_apply x
Recovery of Element via Isometric Self-Equivalence: $e(e^{-1}(x)) = x$
Informal description
For any isometric self-equivalence $e \colon \alpha \simeq \alpha$ of a pseudo-emetric space $\alpha$ and any element $x \in \alpha$, applying $e$ to the inverse image $e^{-1}(x)$ recovers the original element $x$, i.e., $e(e^{-1}(x)) = x$.
IsometryEquiv.completeSpace_iff theorem
(e : α ≃ᵢ β) : CompleteSpace α ↔ CompleteSpace β
Full source 
theorem completeSpace_iff (e : α ≃ᵢ β) : CompleteSpaceCompleteSpace α ↔ CompleteSpace β := by
  simp only [completeSpace_iff_isComplete_univ, ← e.range_eq_univ, ← image_univ,
    isComplete_image_iff e.isometry.isUniformInducing]
Isometric Equivalence Preserves Completeness
Informal description
For any isometric equivalence $e \colon \alpha \simeq \beta$ between two pseudo-emetric spaces, the space $\alpha$ is complete if and only if $\beta$ is complete.
IsometryEquiv.completeSpace theorem
[CompleteSpace β] (e : α ≃ᵢ β) : CompleteSpace α
Full source 
protected theorem completeSpace [CompleteSpace β] (e : α ≃ᵢ β) : CompleteSpace α :=
  e.completeSpace_iff.2 ‹_›
Completeness Transfer via Isometric Equivalence
Informal description
Let $\alpha$ and $\beta$ be pseudo-emetric spaces, and let $e \colon \alpha \simeq \beta$ be an isometric equivalence. If $\beta$ is complete, then $\alpha$ is also complete.
IsometryEquiv.piCongrLeft' definition
{ι' : Type*} [Fintype ι] [Fintype ι'] {Y : ι → Type*} [∀ j, PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : (∀ i, Y i) ≃ᵢ ∀ j, Y (e.symm j)
Full source 
/-- The natural isometry `∀ i, Y i ≃ᵢ ∀ j, Y (e.symm j)` obtained from a bijection `ι ≃ ι'` of
fintypes. `Equiv.piCongrLeft'` as an `IsometryEquiv`. -/
@[simps!]
def piCongrLeft' {ι' : Type*} [Fintype ι] [Fintype ι'] {Y : ι → Type*}
    [∀ j, PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : (∀ i, Y i) ≃ᵢ ∀ j, Y (e.symm j) where
  toEquiv := Equiv.piCongrLeft' _ e
  isometry_toFun x1 x2 := by
    simp_rw [edist_pi_def, Finset.sup_univ_eq_iSup]
    exact (Equiv.iSup_comp (g := fun b ↦ edist (x1 b) (x2 b)) e.symm)
Isometric equivalence of product spaces under index bijection
Informal description
Given finite types $\iota$ and $\iota'$, a family of pseudo-emetric spaces $(Y_i)_{i \in \iota}$, and a bijection $e : \iota \simeq \iota'$, the natural isometry $\big(\prod_{i \in \iota} Y_i\big) \simeq \big(\prod_{j \in \iota'} Y_{e^{-1}(j)}\big)$ is defined by reindexing the product via $e$. Specifically, the isometry maps a function $f : \prod_{i \in \iota} Y_i$ to the function $j \mapsto f(e^{-1}(j))$, preserving the edistance between any two functions.
IsometryEquiv.piCongrLeft definition
{ι' : Type*} [Fintype ι] [Fintype ι'] {Y : ι' → Type*} [∀ j, PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : (∀ i, Y (e i)) ≃ᵢ ∀ j, Y j
Full source 
/-- The natural isometry `∀ i, Y (e i) ≃ᵢ ∀ j, Y j` obtained from a bijection `ι ≃ ι'` of fintypes.
`Equiv.piCongrLeft` as an `IsometryEquiv`. -/
@[simps!]
def piCongrLeft {ι' : Type*} [Fintype ι] [Fintype ι'] {Y : ι' → Type*}
    [∀ j, PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : (∀ i, Y (e i)) ≃ᵢ ∀ j, Y j :=
  (piCongrLeft' e.symm).symm
Isometric equivalence of reindexed product spaces
Informal description
Given finite types $\iota$ and $\iota'$, a family of pseudo-emetric spaces $(Y_j)_{j \in \iota'}$, and a bijection $e : \iota \simeq \iota'$, the natural isometry $\big(\prod_{i \in \iota} Y_{e(i)}\big) \simeq \big(\prod_{j \in \iota'} Y_j\big)$ is defined by reindexing the product via $e$. Specifically, the isometry maps a function $f : \prod_{i \in \iota} Y_{e(i)}$ to the function $j \mapsto f(e^{-1}(j))$, preserving the edistance between any two functions.
IsometryEquiv.sumArrowIsometryEquivProdArrow definition
[Fintype α] [Fintype β] : (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)
Full source 
/-- The natural isometry `(α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)` between the type of maps on a sum of
fintypes `α ⊕ β` and the pairs of functions on the types `α` and `β`.
`Equiv.sumArrowEquivProdArrow` as an `IsometryEquiv`. -/
@[simps!]
def sumArrowIsometryEquivProdArrow [Fintype α] [Fintype β] : (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ) where
  toEquiv := Equiv.sumArrowEquivProdArrow _ _ _
  isometry_toFun _ _ := by simp [Prod.edist_eq, edist_pi_def, Finset.sup_univ_eq_iSup, iSup_sum]
Isometric equivalence between functions on a sum type and product of functions
Informal description
For finite types $\alpha$ and $\beta$, the natural isometry between the space of functions from the sum type $\alpha \oplus \beta$ to a pseudo-emetric space $\gamma$ and the product space of functions from $\alpha$ to $\gamma$ and functions from $\beta$ to $\gamma$. This isometry preserves the edistance, meaning that the edistance between two functions on the sum type equals the maximum of the edistances between their restrictions to $\alpha$ and $\beta$.
IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph theorem
{α β : Type*} [Fintype α] [Fintype β] : sumArrowIsometryEquivProdArrow.toHomeomorph = Homeomorph.sumArrowHomeomorphProdArrow (ι := α) (ι' := β) (X := γ)
Full source 
@[simp]
theorem sumArrowIsometryEquivProdArrow_toHomeomorph {α β : Type*} [Fintype α] [Fintype β] :
    sumArrowIsometryEquivProdArrow.toHomeomorph
    = Homeomorph.sumArrowHomeomorphProdArrow (ι := α) (ι' := β) (X := γ) :=
  rfl
Isometric-Homeomorphic Commutative Diagram for Function Spaces on Sum and Product Types
Informal description
For finite types $\alpha$ and $\beta$, the homeomorphism induced by the isometric equivalence between functions on the sum type $\alpha \oplus \beta$ and the product of functions on $\alpha$ and $\beta$ is equal to the canonical homeomorphism between these function spaces. That is, the following diagram commutes: \[ (\alpha \oplus \beta \to \gamma) \simeq_{\text{isom}} (\alpha \to \gamma) \times (\beta \to \gamma) \simeq_{\text{homeo}} (\alpha \to \gamma) \times (\beta \to \gamma) \] where the first equivalence is the isometric equivalence and the second is the canonical homeomorphism.
Fin.edist_append_eq_max_edist theorem
(m n : ℕ) {x x2 : Fin m → α} {y y2 : Fin n → α} : edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2)
Full source 
theorem _root_.Fin.edist_append_eq_max_edist (m n : ℕ) {x x2 : Fin m → α} {y y2 : Fin n → α} :
    edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2) := by
  simp [edist_pi_def, Finset.sup_univ_eq_iSup, ← Equiv.iSup_comp (e := finSumFinEquiv),
    Prod.edist_eq, iSup_sum]
Extended Distance of Concatenated Functions Equals Maximum of Component Distances
Informal description
For any natural numbers $m$ and $n$, and any pairs of functions $x, x_2 : \text{Fin}\, m \to \alpha$ and $y, y_2 : \text{Fin}\, n \to \alpha$, the extended distance between the concatenated functions $\text{Fin.append}\, x\, y$ and $\text{Fin.append}\, x_2\, y_2$ is equal to the maximum of the extended distances between $x$ and $x_2$ and between $y$ and $y_2$. That is, \[ \text{edist}\, (\text{Fin.append}\, x\, y)\, (\text{Fin.append}\, x_2\, y_2) = \max\, (\text{edist}\, x\, x_2)\, (\text{edist}\, y\, y_2). \]
Fin.appendIsometry definition
(m n : ℕ) : (Fin m → α) × (Fin n → α) ≃ᵢ (Fin (m + n) → α)
Full source 
/-- The natural `IsometryEquiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α`.
`Fin.appendEquiv` as an `IsometryEquiv`. -/
@[simps!]
def _root_.Fin.appendIsometry (m n : ℕ) : (Fin m → α) × (Fin n → α)(Fin m → α) × (Fin n → α) ≃ᵢ (Fin (m + n) → α) where
  toEquiv := Fin.appendEquiv _ _
  isometry_toFun _ _ := by simp_rw [Fin.appendEquiv, Fin.edist_append_eq_max_edist, Prod.edist_eq]
Isometric equivalence for concatenated functions on finite types
Informal description
The natural isometric equivalence between the product space $( \text{Fin}\, m \to \alpha ) \times ( \text{Fin}\, n \to \alpha )$ and the function space $\text{Fin}\, (m + n) \to \alpha$, where $\alpha$ is a pseudo-emetric space. Given a pair of functions $(f, g)$ where $f : \text{Fin}\, m \to \alpha$ and $g : \text{Fin}\, n \to \alpha$, the forward map constructs their concatenation $h : \text{Fin}\, (m + n) \to \alpha$ such that for $i < m$, $h\, i = f\, i$, and for $m \leq i < m + n$, $h\, i = g\, (i - m)$. The inverse map splits a function $h : \text{Fin}\, (m + n) \to \alpha$ into two functions $f : \text{Fin}\, m \to \alpha$ and $g : \text{Fin}\, n \to \alpha$ by restricting $h$ to the appropriate subdomains. This equivalence preserves the edistance, meaning that the edistance between two concatenated functions is the maximum of the edistances between their respective components.
Fin.appendIsometry_toHomeomorph theorem
(m n : ℕ) : (Fin.appendIsometry m n).toHomeomorph = Fin.appendHomeomorph (X := α) m n
Full source 
@[simp]
theorem _root_.Fin.appendIsometry_toHomeomorph (m n : ℕ) :
    (Fin.appendIsometry m n).toHomeomorph = Fin.appendHomeomorph (X := α) m n :=
  rfl
Homeomorphism Equality for Concatenated Functions on Finite Types
Informal description
For any natural numbers $m$ and $n$, the homeomorphism induced by the isometric equivalence `Fin.appendIsometry m n` is equal to the homeomorphism `Fin.appendHomeomorph m n` on the pseudo-emetric space $\alpha$.
IsometryEquiv.funUnique definition
[Unique ι] [Fintype ι] : (ι → α) ≃ᵢ α
Full source 
/-- `Equiv.funUnique` as an `IsometryEquiv`. -/
@[simps!]
def funUnique [Unique ι] [Fintype ι] : (ι → α) ≃ᵢ α where
  toEquiv := Equiv.funUnique ι α
  isometry_toFun x hx := by simp [edist_pi_def, Finset.univ_unique, Finset.sup_singleton]
Isometric equivalence between functions from a singleton type and their codomain
Informal description
Given a type $\iota$ with a unique element and a pseudo-emetric space $\alpha$, the space of functions from $\iota$ to $\alpha$ is isometrically equivalent to $\alpha$ itself. The equivalence maps a function $f : \iota \to \alpha$ to its value at the unique element of $\iota$, and conversely, any element $a \in \alpha$ can be viewed as the constant function sending the unique element of $\iota$ to $a$. This equivalence preserves the edistance, meaning that the edistance between two functions is equal to the edistance between their corresponding values in $\alpha$.
IsometryEquiv.piFinTwo definition
(α : Fin 2 → Type*) [∀ i, PseudoEMetricSpace (α i)] : (∀ i, α i) ≃ᵢ α 0 × α 1
Full source 
/-- `piFinTwoEquiv` as an `IsometryEquiv`. -/
@[simps!]
def piFinTwo (α : Fin 2 → Type*) [∀ i, PseudoEMetricSpace (α i)] : (∀ i, α i) ≃ᵢ α 0 × α 1 where
  toEquiv := piFinTwoEquiv α
  isometry_toFun x hx := by simp [edist_pi_def, Fin.univ_succ, Prod.edist_eq]
Isometric equivalence between dependent functions on `Fin 2` and pairs
Informal description
The isometric equivalence `IsometryEquiv.piFinTwo` establishes a bijection between the space of dependent functions on `Fin 2` (i.e., pairs of elements where the first is of type `α 0` and the second is of type `α 1`) and the Cartesian product `α 0 × α 1`, preserving the pseudo-emetric structure. Specifically, for any two elements in the function space, their edistance is equal to the edistance between their corresponding pairs in the product space.
IsometryEquiv.diam_image theorem
(s : Set α) : Metric.diam (h '' s) = Metric.diam s
Full source 
@[simp]
theorem diam_image (s : Set α) : Metric.diam (h '' s) = Metric.diam s :=
  h.isometry.diam_image s
Isometric Equivalence Preserves Diameter of Subsets
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudometric spaces $\alpha$ and $\beta$, and for any subset $s \subseteq \alpha$, the diameter of the image $h(s)$ in $\beta$ is equal to the diameter of $s$ in $\alpha$, i.e., \[ \text{diam}(h(s)) = \text{diam}(s). \]
IsometryEquiv.diam_preimage theorem
(s : Set β) : Metric.diam (h ⁻¹' s) = Metric.diam s
Full source 
@[simp]
theorem diam_preimage (s : Set β) : Metric.diam (h ⁻¹' s) = Metric.diam s := by
  rw [← image_symm, diam_image]
Isometric Equivalence Preserves Diameter of Preimages
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudometric spaces $\alpha$ and $\beta$, and for any subset $s \subseteq \beta$, the diameter of the preimage $h^{-1}(s)$ in $\alpha$ is equal to the diameter of $s$ in $\beta$, i.e., \[ \text{diam}(h^{-1}(s)) = \text{diam}(s). \]
IsometryEquiv.diam_univ theorem
: Metric.diam (univ : Set α) = Metric.diam (univ : Set β)
Full source 
theorem diam_univ : Metric.diam (univ : Set α) = Metric.diam (univ : Set β) :=
  congr_arg ENNReal.toReal h.ediam_univ
Isometric Equivalence Preserves Diameter of Universal Sets
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudometric spaces $\alpha$ and $\beta$, the diameter of the universal set in $\alpha$ is equal to the diameter of the universal set in $\beta$, i.e., \[ \text{diam}(\text{univ} \subseteq \alpha) = \text{diam}(\text{univ} \subseteq \beta). \]
IsometryEquiv.preimage_ball theorem
(h : α ≃ᵢ β) (x : β) (r : ℝ) : h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r
Full source 
@[simp]
theorem preimage_ball (h : α ≃ᵢ β) (x : β) (r : ℝ) :
    h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r := by
  rw [← h.isometry.preimage_ball (h.symm x) r, h.apply_symm_apply]
Isometric Equivalence Preserves Open Ball Preimages: $h^{-1}(\mathrm{ball}(x, r)) = \mathrm{ball}(h^{-1}(x), r)$
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudometric spaces, and let $x \in \beta$ and $r \in \mathbb{R}$. Then the preimage under $h$ of the open ball $\mathrm{ball}(x, r)$ in $\beta$ is equal to the open ball $\mathrm{ball}(h^{-1}(x), r)$ in $\alpha$, i.e., $$ h^{-1}(\mathrm{ball}(x, r)) = \mathrm{ball}(h^{-1}(x), r). $$
IsometryEquiv.preimage_sphere theorem
(h : α ≃ᵢ β) (x : β) (r : ℝ) : h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r
Full source 
@[simp]
theorem preimage_sphere (h : α ≃ᵢ β) (x : β) (r : ℝ) :
    h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r := by
  rw [← h.isometry.preimage_sphere (h.symm x) r, h.apply_symm_apply]
Isometric Equivalence Preserves Sphere Preimages: $h^{-1}(S(x, r)) = S(h^{-1}(x), r)$
Informal description
For any isometric equivalence $h \colon \alpha \simeq \beta$ between two pseudometric spaces, any point $x \in \beta$, and any radius $r \in \mathbb{R}$, the preimage under $h$ of the sphere centered at $x$ with radius $r$ is equal to the sphere centered at $h^{-1}(x)$ with radius $r$, i.e., $$ h^{-1}(\{y \in \beta \mid \text{dist}(y, x) = r\}) = \{y \in \alpha \mid \text{dist}(y, h^{-1}(x)) = r\}. $$
IsometryEquiv.preimage_closedBall theorem
(h : α ≃ᵢ β) (x : β) (r : ℝ) : h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r
Full source 
@[simp]
theorem preimage_closedBall (h : α ≃ᵢ β) (x : β) (r : ℝ) :
    h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r := by
  rw [← h.isometry.preimage_closedBall (h.symm x) r, h.apply_symm_apply]
Isometric Equivalence Preserves Closed Balls: $h^{-1}(\overline{B}(x, r)) = \overline{B}(h^{-1}(x), r)$
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudometric spaces. For any point $x \in \beta$ and radius $r \in \mathbb{R}$, the preimage under $h$ of the closed ball $\overline{B}(x, r)$ in $\beta$ is equal to the closed ball $\overline{B}(h^{-1}(x), r)$ in $\alpha$, i.e., $$ h^{-1}(\overline{B}(x, r)) = \overline{B}(h^{-1}(x), r). $$
IsometryEquiv.image_ball theorem
(h : α ≃ᵢ β) (x : α) (r : ℝ) : h '' Metric.ball x r = Metric.ball (h x) r
Full source 
@[simp]
theorem image_ball (h : α ≃ᵢ β) (x : α) (r : ℝ) : h '' Metric.ball x r = Metric.ball (h x) r := by
  rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]
Isometric Equivalence Preserves Open Ball Images: $h(B(x, r)) = B(h(x), r)$
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudometric spaces. For any point $x \in \alpha$ and radius $r > 0$, the image under $h$ of the open ball $\mathrm{ball}(x, r)$ in $\alpha$ is equal to the open ball $\mathrm{ball}(h(x), r)$ in $\beta$, i.e., $$ h(\mathrm{ball}(x, r)) = \mathrm{ball}(h(x), r). $$
IsometryEquiv.image_sphere theorem
(h : α ≃ᵢ β) (x : α) (r : ℝ) : h '' Metric.sphere x r = Metric.sphere (h x) r
Full source 
@[simp]
theorem image_sphere (h : α ≃ᵢ β) (x : α) (r : ℝ) :
    h '' Metric.sphere x r = Metric.sphere (h x) r := by
  rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]
Isometric Equivalence Preserves Spheres: $h(S(x, r)) = S(h(x), r)$
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudometric spaces. For any point $x \in \alpha$ and radius $r \in \mathbb{R}$, the image under $h$ of the sphere centered at $x$ with radius $r$ is equal to the sphere centered at $h(x)$ with radius $r$, i.e., $$ h(\{y \in \alpha \mid \text{dist}(y, x) = r\}) = \{y \in \beta \mid \text{dist}(y, h(x)) = r\}. $$
IsometryEquiv.image_closedBall theorem
(h : α ≃ᵢ β) (x : α) (r : ℝ) : h '' Metric.closedBall x r = Metric.closedBall (h x) r
Full source 
@[simp]
theorem image_closedBall (h : α ≃ᵢ β) (x : α) (r : ℝ) :
    h '' Metric.closedBall x r = Metric.closedBall (h x) r := by
  rw [← h.preimage_symm, h.symm.preimage_closedBall, symm_symm]
Isometric Equivalence Preserves Closed Balls: $h(\overline{B}(x, r)) = \overline{B}(h(x), r)$
Informal description
Let $h \colon \alpha \simeq \beta$ be an isometric equivalence between two pseudometric spaces. For any point $x \in \alpha$ and radius $r \in \mathbb{R}$, the image under $h$ of the closed ball $\overline{B}(x, r)$ in $\alpha$ is equal to the closed ball $\overline{B}(h(x), r)$ in $\beta$, i.e., $$ h(\overline{B}(x, r)) = \overline{B}(h(x), r). $$
Isometry.isometryEquivOnRange definition
[EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) : α ≃ᵢ range f
Full source 
/-- An isometry induces an isometric isomorphism between the source space and the
range of the isometry. -/
@[simps! +simpRhs toEquiv apply]
def Isometry.isometryEquivOnRange [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β}
    (h : Isometry f) : α ≃ᵢ range f where
  isometry_toFun := h
  toEquiv := Equiv.ofInjective f h.injective
Isometric equivalence between domain and range of an isometry
Informal description
Given an isometry \( f \colon \alpha \to \beta \) between an emetric space \( \alpha \) and a pseudoemetric space \( \beta \), there exists an isometric equivalence between \( \alpha \) and the range of \( f \). This equivalence is constructed by restricting the codomain of \( f \) to its range and using the injectivity of \( f \).
Isometry.lipschitzWith_iff theorem
{α β γ : Type*} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : α → β} {g : β → γ} (K : ℝ≥0) (h : Isometry g) : LipschitzWith K (g ∘ f) ↔ LipschitzWith K f
Full source 
/-- Post-composition by an isometry does not change the Lipschitz-property of a function. -/
lemma Isometry.lipschitzWith_iff {α β γ : Type*} [PseudoEMetricSpace α] [PseudoEMetricSpace β]
    [PseudoEMetricSpace γ] {f : α → β} {g : β → γ} (K : ℝ≥0) (h : Isometry g) :
    LipschitzWithLipschitzWith K (g ∘ f) ↔ LipschitzWith K f := by
  simp [LipschitzWith, h.edist_eq]
Lipschitz Property Preservation under Post-Composition by Isometry
Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be maps between pseudoemetric spaces, and let $K \in \mathbb{R}_{\geq 0}$. If $g$ is an isometry, then the composition $g \circ f$ is $K$-Lipschitz if and only if $f$ is $K$-Lipschitz. In other words, for an isometry $g$, the Lipschitz constant of $g \circ f$ equals that of $f$.