# mathlibdocumentation

topology.metric_space.isometry

# 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.

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

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

Equations
theorem isometry_emetric_iff_metric {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :
∀ (x y : α), dist (f x) (f y) = dist x y

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

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

An isometry preserves edistances.

theorem isometry.dist_eq {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} (hf : isometry f) (x y : α) :
dist (f x) (f y) = dist x y

An isometry preserves distances.

theorem isometry.lipschitz {α : Type u} {β : Type v} {f : α → β} :

theorem isometry.antilipschitz {α : Type u} {β : Type v} {f : α → β} :

theorem isometry.injective {α : Type u} {β : Type v} {f : α → β} :

An isometry is injective

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.comp {α : Type u} {β : Type v} {γ : Type w} {g : β → γ} {f : α → β} :
isometry (g f)

The composition of isometries is an isometry

theorem isometry.uniform_embedding {α : Type u} {β : Type v} {f : α → β} :

An isometry is an embedding

theorem isometry.continuous {α : Type u} {β : Type v} {f : α → β} :

An isometry is continuous.

theorem isometry.right_inv {α : Type u} {β : Type v} {f : α → β} {g : β → α} :

The right inverse of an isometry is an isometry.

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

Isometries preserve the diameter in emetric spaces.

theorem isometry.ediam_range {α : Type u} {β : Type v} {f : α → β} :

theorem isometry_subtype_coe {α : Type u} {s : set α} :

The injection from a subtype is an isometry

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

An isometry preserves the diameter in metric spaces.

theorem isometry.diam_range {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :

@[nolint]
structure isometric (α : Type u_1) (β : Type u_2)  :
Type (max u_1 u_2)
• to_equiv : α β
• isometry_to_fun :

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

@[instance]
def isometric.has_coe_to_fun {α : Type u} {β : Type v}  :

Equations
theorem isometric.coe_eq_to_equiv {α : Type u} {β : Type v} (h : α ≃ᵢ β) (a : α) :
h a = (h.to_equiv) a

@[simp]
theorem isometric.coe_to_equiv {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

theorem isometric.isometry {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

theorem isometric.edist_eq {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x y : α) :
edist (h x) (h y) = y

theorem isometric.dist_eq {α : Type u_1} {β : Type u_2} [metric_space α] [metric_space β] (h : α ≃ᵢ β) (x y : α) :
dist (h x) (h y) = dist x y

theorem isometric.continuous {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

theorem isometric.to_equiv_inj {α : Type u} {β : Type v} ⦃h₁ h₂ : α ≃ᵢ β⦄ :
h₁.to_equiv = h₂.to_equivh₁ = h₂

@[ext]
theorem isometric.ext {α : Type u} {β : Type v} ⦃h₁ h₂ : α ≃ᵢ β⦄ :
(∀ (x : α), h₁ x = h₂ x)h₁ = h₂

def isometric.mk' {α : Type u} {β : Type v} (f : α → β) (g : β → α) :
(∀ (x : β), f (g x) = x)α ≃ᵢ β

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

Equations
def isometric.refl (α : Type u_1)  :
α ≃ᵢ α

The identity isometry of a space.

Equations
def isometric.trans {α : Type u} {β : Type v} {γ : Type w}  :
α ≃ᵢ ββ ≃ᵢ γα ≃ᵢ γ

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

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

def isometric.symm {α : Type u} {β : Type v}  :
α ≃ᵢ ββ ≃ᵢ α

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

Equations
@[simp]
theorem isometric.symm_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
h.symm.symm = h

@[simp]
theorem isometric.apply_symm_apply {α : Type u} {β : Type v} (h : α ≃ᵢ β) (y : β) :
h ((h.symm) y) = y

@[simp]
theorem isometric.symm_apply_apply {α : Type u} {β : Type v} (h : α ≃ᵢ β) (x : α) :
(h.symm) (h x) = x

theorem isometric.symm_apply_eq {α : Type u} {β : Type v} (h : α ≃ᵢ β) {x : α} {y : β} :
(h.symm) y = x y = h x

theorem isometric.eq_symm_apply {α : Type u} {β : Type v} (h : α ≃ᵢ β) {x : α} {y : β} :
x = (h.symm) y h x = y

theorem isometric.symm_comp_self {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

theorem isometric.self_comp_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

theorem isometric.range_coe {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

theorem isometric.image_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

theorem isometric.preimage_symm {α : Type u} {β : Type v} (h : α ≃ᵢ β) :
=

@[simp]
theorem isometric.symm_trans_apply {α : Type u} {β : Type v} {γ : Type w} (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : γ) :
((h₁.trans h₂).symm) x = (h₁.symm) ((h₂.symm) x)

def isometric.to_homeomorph {α : Type u} {β : Type v}  :
α ≃ᵢ βα ≃ₜ β

The (bundled) homeomorphism associated to an isometric isomorphism.

Equations
@[simp]
theorem isometric.coe_to_homeomorph {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

@[simp]
theorem isometric.to_homeomorph_to_equiv {α : Type u} {β : Type v} (h : α ≃ᵢ β) :

@[instance]
def isometric.group {α : Type u}  :
group ≃ᵢ α)

The group of isometries.

Equations
@[simp]
theorem isometric.coe_one {α : Type u}  :

@[simp]
theorem isometric.coe_mul {α : Type u} (e₁ e₂ : α ≃ᵢ α) :
e₁ * e₂ = e₂ e₁

theorem isometric.mul_apply {α : Type u} (e₁ e₂ : α ≃ᵢ α) (x : α) :
(e₁ * e₂) x = e₂ (e₁ x)

@[simp]
theorem isometric.inv_apply_self {α : Type u} (e : α ≃ᵢ α) (x : α) :
e⁻¹ (e x) = x

@[simp]
theorem isometric.apply_inv_self {α : Type u} (e : α ≃ᵢ α) (x : α) :
e (e⁻¹ x) = x

def isometric.add_right {G : Type u_1} [normed_group G] :
G → G ≃ᵢ G

Addition y ↦ y + x as an isometry.

Equations
@[simp]
theorem isometric.add_right_to_equiv {G : Type u_1} [normed_group G] (x : G) :

@[simp]
theorem isometric.coe_add_right {G : Type u_1} [normed_group G] (x : G) :
= λ (y : G), y + x

theorem isometric.add_right_apply {G : Type u_1} [normed_group G] (x y : G) :
y = y + x

@[simp]
theorem isometric.add_right_symm {G : Type u_1} [normed_group G] (x : G) :

def isometric.add_left {G : Type u_1} [normed_group G] :
G → G ≃ᵢ G

Addition y ↦ x + y as an isometry.

Equations
@[simp]
theorem isometric.add_left_to_equiv {G : Type u_1} [normed_group G] (x : G) :

@[simp]
theorem isometric.coe_add_left {G : Type u_1} [normed_group G] (x : G) :

@[simp]
theorem isometric.add_left_symm {G : Type u_1} [normed_group G] (x : G) :

def isometric.neg (G : Type u_1) [normed_group G] :
G ≃ᵢ G

Negation x ↦ -x as an isometry.

Equations
@[simp]
theorem isometric.neg_symm {G : Type u_1} [normed_group G] :

@[simp]
theorem isometric.neg_to_equiv {G : Type u_1} [normed_group G] :

@[simp]
theorem isometric.coe_neg {G : Type u_1} [normed_group G] :

def isometry.isometric_on_range {α : Type u} {β : Type v} {f : α → β} :
α ≃ᵢ (set.range f)

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

Equations
@[simp]
theorem isometry.isometric_on_range_apply {α : Type u} {β : Type v} {f : α → β} (h : isometry f) (x : α) :
(h.isometric_on_range) x = f x, _⟩

theorem algebra_map_isometry (𝕜 : Type u_1) (𝕜' : Type u_2) [normed_field 𝕜] [normed_ring 𝕜'] [ 𝕜'] :
isometry 𝕜')

In a normed algebra, the inclusion of the base field in the extended field is an isometry.

def ℓ_infty_ℝ  :
Type

The space of bounded sequences, with its sup norm

Equations

### In this section, we show that any separable metric space can be embedded isometrically in ℓ^∞(ℝ)

def Kuratowski_embedding.embedding_of_subset {α : Type u} [metric_space α] :
( → α)α → ℓ_infty_ℝ

A metric space can be embedded in l^∞(ℝ) via the distances to points in a fixed countable set, if this set is dense. This map is given in the next definition, without density assumptions.

Equations
theorem Kuratowski_embedding.embedding_of_subset_coe {α : Type u} {n : } [metric_space α] (x : → α) (a : α) :
= dist a (x n) - dist (x 0) (x n)

theorem Kuratowski_embedding.embedding_of_subset_dist_le {α : Type u} [metric_space α] (x : → α) (a b : α) :

The embedding map is always a semi-contraction.

theorem Kuratowski_embedding.embedding_of_subset_isometry {α : Type u} [metric_space α] (x : → α) :

When the reference set is dense, the embedding map is an isometry on its image.

theorem Kuratowski_embedding.exists_isometric_embedding (α : Type u) [metric_space α]  :
∃ (f : α → ℓ_infty_ℝ),

Every separable metric space embeds isometrically in ℓ_infty_ℝ.

def Kuratowski_embedding (α : Type u) [metric_space α]  :

The Kuratowski embedding is an isometric embedding of a separable metric space in ℓ^∞(ℝ)

Equations
theorem Kuratowski_embedding.isometry (α : Type u) [metric_space α]  :

The Kuratowski embedding is an isometry

Version of the Kuratowski embedding for nonempty compacts

Equations