# mathlib3documentation

topology.metric_space.isometry

# Isometries #

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

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 pseudo_metric_space and we specialize to metric_space when needed.

def isometry {α : Type u} {β : Type v} (f : α β) :
Prop

An isometry (also known as isometric embedding) is a map preserving the edistance between pseudoemetric spaces, or equivalently the distance between pseudometric space.

Equations
theorem isometry_iff_nndist_eq {α : Type u} {β : Type v} {f : α β} :
(x y : α), has_nndist.nndist (f x) (f y) =

On pseudometric spaces, a map is an isometry if and only if it preserves nonnegative distances.

theorem isometry_iff_dist_eq {α : Type u} {β : Type v} {f : α β} :
(x y : α), has_dist.dist (f x) (f y) =

On pseudometric spaces, a map is an isometry if and only if it preserves distances.

theorem isometry.dist_eq {α : Type u} {β : Type v} {f : α β} :
(x y : α), has_dist.dist (f x) (f y) =

An isometry preserves distances.

theorem isometry.of_dist_eq {α : Type u} {β : Type v} {f : α β} :
( (x y : α), has_dist.dist (f x) (f y) = y)

A map that preserves distances is an isometry

theorem isometry.nndist_eq {α : Type u} {β : Type v} {f : α β} :
(x y : α), has_nndist.nndist (f x) (f y) =

An isometry preserves non-negative distances.

theorem isometry.of_nndist_eq {α : Type u} {β : Type v} {f : α β} :
( (x y : α), has_nndist.nndist (f x) (f y) =

A map that preserves non-negative distances is an isometry.

theorem isometry.edist_eq {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x y : α) :
has_edist.edist (f x) (f y) =

An isometry preserves edistances.

theorem isometry.lipschitz {α : Type u} {β : Type v} {f : α β} (h : isometry f) :
theorem isometry.antilipschitz {α : Type u} {β : Type v} {f : α β} (h : isometry f) :
theorem isometry_subsingleton {α : Type u} {β : Type v} {f : α β} [subsingleton α] :

Any map on a subsingleton is an isometry

theorem isometry_id {α : Type u}  :

The identity is an isometry

theorem isometry.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : α β} {g : γ δ} (hf : isometry f) (hg : isometry g) :
theorem isometry_dcomp {ι : Type u_1} [fintype ι] {α : ι Type u_2} {β : ι Type u_3} [Π (i : ι), pseudo_emetric_space (α i)] [Π (i : ι), pseudo_emetric_space (β i)] (f : Π (i : ι), α i β i) (hf : (i : ι), isometry (f i)) :
theorem isometry.comp {α : Type u} {β : Type v} {γ : Type w} {g : β γ} {f : α β} (hg : isometry g) (hf : isometry f) :

The composition of isometries is an isometry.

@[protected]
theorem isometry.uniform_continuous {α : Type u} {β : Type v} {f : α β} (hf : isometry f) :

An isometry from a metric space is a uniform continuous map

@[protected]
theorem isometry.uniform_inducing {α : Type u} {β : Type v} {f : α β} (hf : isometry f) :

An isometry from a metric space is a uniform inducing map

theorem isometry.tendsto_nhds_iff {α : Type u} {β : Type v} {ι : Type u_1} {f : α β} {g : ι α} {a : filter ι} {b : α} (hf : isometry f) :
(nhds b) filter.tendsto (f g) a (nhds (f b))
@[protected]
theorem isometry.continuous {α : Type u} {β : Type v} {f : α β} (hf : isometry f) :

An isometry is continuous.

theorem isometry.right_inv {α : Type u} {β : Type v} {f : α β} {g : β α} (h : isometry f) (hg : f) :

The right inverse of an isometry is an isometry.

theorem isometry.preimage_emetric_closed_ball {α : Type u} {β : Type v} {f : α β} (h : isometry f) (x : α) (r : ennreal) :
theorem isometry.preimage_emetric_ball {α : Type u} {β : Type v} {f : α β} (h : isometry f) (x : α) (r : ennreal) :
f ⁻¹' emetric.ball (f x) r = r
theorem isometry.ediam_image {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (s : set α) :

Isometries preserve the diameter in pseudoemetric spaces.

theorem isometry.ediam_range {α : Type u} {β : Type v} {f : α β} (hf : isometry f) :
theorem isometry.maps_to_emetric_ball {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (r : ennreal) :
r) (emetric.ball (f x) r)
theorem isometry.maps_to_emetric_closed_ball {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (r : ennreal) :
r) (emetric.closed_ball (f x) r)
theorem isometry_subtype_coe {α : Type u} {s : set α} :

The injection from a subtype is an isometry

theorem isometry.comp_continuous_on_iff {α : Type u} {β : Type v} {f : α β} {γ : Type u_1} (hf : isometry f) {g : γ α} {s : set γ} :
theorem isometry.comp_continuous_iff {α : Type u} {β : Type v} {f : α β} {γ : Type u_1} (hf : isometry f) {g : γ α} :
@[protected]
theorem isometry.injective {α : Type u} {β : Type v} {f : α β} (h : isometry f) :

An isometry from an emetric space is injective

@[protected]
theorem isometry.uniform_embedding {α : Type u} {β : Type v} {f : α β} (hf : isometry f) :

An isometry from an emetric space is a uniform embedding

@[protected]
theorem isometry.embedding {α : Type u} {β : Type v} {f : α β} (hf : isometry f) :

An isometry from an emetric space is an embedding

theorem isometry.closed_embedding {α : Type u} {γ : Type w} {f : α γ} (hf : isometry f) :

An isometry from a complete emetric space is a closed embedding

theorem isometry.diam_image {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (s : set α) :

An isometry preserves the diameter in pseudometric spaces.

theorem isometry.diam_range {α : Type u} {β : Type v} {f : α β} (hf : isometry f) :
theorem isometry.preimage_set_of_dist {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (p : Prop) :
f ⁻¹' {y : β | p (f x))} = {y : α | p x)}
theorem isometry.preimage_closed_ball {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (r : ) :
theorem isometry.preimage_ball {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (r : ) :
f ⁻¹' metric.ball (f x) r = r
theorem isometry.preimage_sphere {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (r : ) :
theorem isometry.maps_to_ball {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (r : ) :
r) (metric.ball (f x) r)
theorem isometry.maps_to_sphere {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (r : ) :
r) (metric.sphere (f x) r)
theorem isometry.maps_to_closed_ball {α : Type u} {β : Type v} {f : α β} (hf : isometry f) (x : α) (r : ) :
r) (metric.closed_ball (f x) r)
theorem uniform_embedding.to_isometry {α : Type u_1} {β : Type u_2} [metric_space β] {f : α β} (h : uniform_embedding f) :

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 embedding.to_isometry {α : Type u_1} {β : Type u_2} [metric_space β] {f : α β} (h : embedding f) :

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.

@[nolint]
structure isometry_equiv (α : Type u_2) (β : Type u_3)  :
Type (max u_2 u_3)

α and β are isometric if there is an isometric bijection between them.

Instances for isometry_equiv
@[protected, instance]
def isometry_equiv.has_coe_to_fun {α : Type u} {β : Type v}  :
has_coe_to_fun ≃ᵢ β) (λ (_x : α ≃ᵢ β), α β)
Equations
theorem isometry_equiv.coe_eq_to_equiv {α : Type u} {β : Type v} (h : α ≃ᵢ β) (a : α) :
h a = (h.to_equiv) a
@[simp]
theorem isometry_equiv.coe_to_equiv {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[protected]
theorem isometry_equiv.isometry {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[protected]
theorem isometry_equiv.bijective {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[protected]
theorem isometry_equiv.injective {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[protected]
theorem isometry_equiv.surjective {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[protected]
theorem isometry_equiv.edist_eq {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x y : α) :
@[protected]
theorem isometry_equiv.dist_eq {α : Type u_1} {β : Type u_2} (h : α ≃ᵢ β) (x y : α) :
has_dist.dist (h x) (h y) =
@[protected]
theorem isometry_equiv.nndist_eq {α : Type u_1} {β : Type u_2} (h : α ≃ᵢ β) (x y : α) :
@[protected]
theorem isometry_equiv.continuous {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[simp]
theorem isometry_equiv.ediam_image {α : Type u} {β : Type v} (h : α ≃ᵢ β) (s : set α) :
theorem isometry_equiv.to_equiv_inj {α : Type u} {β : Type v} ⦃h₁ h₂ : α ≃ᵢ β⦄ :
h₁.to_equiv = h₂.to_equiv h₁ = h₂
@[ext]
theorem isometry_equiv.ext {α : Type u} {β : Type v} ⦃h₁ h₂ : α ≃ᵢ β⦄ (H : (x : α), h₁ x = h₂ x) :
h₁ = h₂
def isometry_equiv.mk' {β : Type v} {α : Type u} (f : α β) (g : β α) (hfg : (x : β), f (g x) = x) (hf : isometry f) :
α ≃ᵢ β

Alternative constructor for isometric bijections, taking as input an isometry, and a right inverse.

Equations
@[protected]
def isometry_equiv.refl (α : Type u_1)  :
α ≃ᵢ α

The identity isometry of a space.

Equations
@[protected]
def isometry_equiv.trans {α : Type u} {β : Type v} {γ : Type w} (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) :
α ≃ᵢ γ

The composition of two isometric isomorphisms, as an isometric isomorphism.

Equations
@[simp]
theorem isometry_equiv.trans_apply {α : Type u} {β : Type v} {γ : Type w} (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : α) :
(h₁.trans h₂) x = h₂ (h₁ x)
@[protected]
def isometry_equiv.symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
β ≃ᵢ α

The inverse of an isometric isomorphism, as an isometric isomorphism.

Equations
def isometry_equiv.simps.apply {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
α β

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
def isometry_equiv.simps.symm_apply {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
β α
Equations
@[simp]
theorem isometry_equiv.symm_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
h.symm.symm = h
@[simp]
theorem isometry_equiv.apply_symm_apply {α : Type u} {β : Type v} (h : α ≃ᵢ β) (y : β) :
h ((h.symm) y) = y
@[simp]
theorem isometry_equiv.symm_apply_apply {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : α) :
(h.symm) (h x) = x
theorem isometry_equiv.symm_apply_eq {α : Type u} {β : Type v} (h : α ≃ᵢ β) {x : α} {y : β} :
(h.symm) y = x y = h x
theorem isometry_equiv.eq_symm_apply {α : Type u} {β : Type v} (h : α ≃ᵢ β) {x : α} {y : β} :
x = (h.symm) y h x = y
theorem isometry_equiv.symm_comp_self {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
theorem isometry_equiv.self_comp_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[simp]
theorem isometry_equiv.range_eq_univ {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
theorem isometry_equiv.image_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
theorem isometry_equiv.preimage_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
=
@[simp]
theorem isometry_equiv.symm_trans_apply {α : Type u} {β : Type v} {γ : Type w} (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : γ) :
((h₁.trans h₂).symm) x = (h₁.symm) ((h₂.symm) x)
theorem isometry_equiv.ediam_univ {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[simp]
theorem isometry_equiv.ediam_preimage {α : Type u} {β : Type v} (h : α ≃ᵢ β) (s : set β) :
@[simp]
theorem isometry_equiv.preimage_emetric_ball {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : β) (r : ennreal) :
@[simp]
theorem isometry_equiv.preimage_emetric_closed_ball {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : β) (r : ennreal) :
@[simp]
theorem isometry_equiv.image_emetric_ball {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : α) (r : ennreal) :
h '' r = emetric.ball (h x) r
@[simp]
theorem isometry_equiv.image_emetric_closed_ball {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : α) (r : ennreal) :
@[protected]
def isometry_equiv.to_homeomorph {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
α ≃ₜ β

The (bundled) homeomorphism associated to an isometric isomorphism.

Equations
@[simp]
theorem isometry_equiv.to_homeomorph_to_equiv {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[simp]
theorem isometry_equiv.coe_to_homeomorph {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[simp]
theorem isometry_equiv.coe_to_homeomorph_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[simp]
theorem isometry_equiv.comp_continuous_on_iff {α : Type u} {β : Type v} {γ : Type u_1} (h : α ≃ᵢ β) {f : γ α} {s : set γ} :
@[simp]
theorem isometry_equiv.comp_continuous_iff {α : Type u} {β : Type v} {γ : Type u_1} (h : α ≃ᵢ β) {f : γ α} :
@[simp]
theorem isometry_equiv.comp_continuous_iff' {α : Type u} {β : Type v} {γ : Type u_1} (h : α ≃ᵢ β) {f : β γ} :
@[protected, instance]
def isometry_equiv.group {α : Type u}  :
group ≃ᵢ α)

The group of isometries.

Equations
@[simp]
theorem isometry_equiv.coe_one {α : Type u}  :
@[simp]
theorem isometry_equiv.coe_mul {α : Type u} (e₁ e₂ : α ≃ᵢ α) :
(e₁ * e₂) = e₁ e₂
theorem isometry_equiv.mul_apply {α : Type u} (e₁ e₂ : α ≃ᵢ α) (x : α) :
(e₁ * e₂) x = e₁ (e₂ x)
@[simp]
theorem isometry_equiv.inv_apply_self {α : Type u} (e : α ≃ᵢ α) (x : α) :
e⁻¹ (e x) = x
@[simp]
theorem isometry_equiv.apply_inv_self {α : Type u} (e : α ≃ᵢ α) (x : α) :
e (e⁻¹ x) = x
@[protected]
theorem isometry_equiv.complete_space {α : Type u} {β : Type v} (e : α ≃ᵢ β) :
theorem isometry_equiv.complete_space_iff {α : Type u} {β : Type v} (e : α ≃ᵢ β) :
def isometry_equiv.fun_unique (ι : Type u_1) (α : Type u) [unique ι] [fintype ι] :
α) ≃ᵢ α

equiv.fun_unique as an isometry_equiv.

Equations
@[simp]
theorem isometry_equiv.fun_unique_apply (ι : Type u_1) (α : Type u) [unique ι] [fintype ι] (f : Π (x : ι), (λ (a' : ι), (λ (ᾰ : ι), α) a') x) :
@[simp]
theorem isometry_equiv.fun_unique_symm_apply (ι : Type u_1) (α : Type u) [unique ι] [fintype ι] (x : α) (b : ι) :
.symm) x b = x
@[simp]
theorem isometry_equiv.fun_unique_to_equiv (ι : Type u_1) (α : Type u) [unique ι] [fintype ι] :
@[simp]
theorem isometry_equiv.pi_fin_two_apply (α : fin 2 Type u_1) [Π (i : fin 2), pseudo_emetric_space (α i)] (f : Π (i : fin 2), α i) :
= (f 0, f 1)
def isometry_equiv.pi_fin_two (α : fin 2 Type u_1) [Π (i : fin 2), pseudo_emetric_space (α i)] :
(Π (i : fin 2), α i) ≃ᵢ α 0 × α 1

pi_fin_two_equiv as an isometry_equiv.

Equations
@[simp]
theorem isometry_equiv.pi_fin_two_symm_apply (α : fin 2 Type u_1) [Π (i : fin 2), pseudo_emetric_space (α i)] (p : α 0 × α 1) (i : fin (1 + 1)) :
p i = i
@[simp]
theorem isometry_equiv.pi_fin_two_to_equiv (α : fin 2 Type u_1) [Π (i : fin 2), pseudo_emetric_space (α i)] :
@[simp]
theorem isometry_equiv.diam_image {α : Type u} {β : Type v} (h : α ≃ᵢ β) (s : set α) :
@[simp]
theorem isometry_equiv.diam_preimage {α : Type u} {β : Type v} (h : α ≃ᵢ β) (s : set β) :
theorem isometry_equiv.diam_univ {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
@[simp]
theorem isometry_equiv.preimage_ball {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : β) (r : ) :
@[simp]
theorem isometry_equiv.preimage_sphere {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : β) (r : ) :
@[simp]
theorem isometry_equiv.preimage_closed_ball {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : β) (r : ) :
@[simp]
theorem isometry_equiv.image_ball {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : α) (r : ) :
h '' r = metric.ball (h x) r
@[simp]
theorem isometry_equiv.image_sphere {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : α) (r : ) :
@[simp]
theorem isometry_equiv.image_closed_ball {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : α) (r : ) :
@[simp]
theorem isometry.isometry_equiv_on_range_to_equiv {α : Type u} {β : Type v} {f : α β} (h : isometry f) :
noncomputable def isometry.isometry_equiv_on_range {α : Type u} {β : Type v} {f : α β} (h : isometry f) :

An isometry induces an isometric isomorphism between the source space and the range of the isometry.

Equations
@[simp]
theorem isometry.isometry_equiv_on_range_apply {α : Type u} {β : Type v} {f : α β} (h : isometry f) (a : α) :