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.
An isometry (also known as isometric embedding) is a map preserving the edistance between emetric spaces, or equivalently the distance between metric space.
Equations
- isometry f = ∀ (x1 x2 : α), has_edist.edist (f x1) (f x2) = has_edist.edist x1 x2
theorem
isometry_emetric_iff_metric
{α : Type u}
{β : Type v}
[metric_space α]
[metric_space β]
{f : α → β} :
isometry f ↔ ∀ (x y : α), has_dist.dist (f x) (f y) = has_dist.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}
[emetric_space α]
[emetric_space β]
{f : α → β}
(hf : isometry f)
(x y : α) :
has_edist.edist (f x) (f y) = has_edist.edist x y
An isometry preserves edistances.
theorem
isometry.dist_eq
{α : Type u}
{β : Type v}
[metric_space α]
[metric_space β]
{f : α → β}
(hf : isometry f)
(x y : α) :
has_dist.dist (f x) (f y) = has_dist.dist x y
An isometry preserves distances.
theorem
isometry.lipschitz
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β} :
isometry f → lipschitz_with 1 f
theorem
isometry.antilipschitz
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β} :
isometry f → antilipschitz_with 1 f
theorem
isometry.injective
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β} :
isometry f → function.injective f
An isometry is injective
theorem
isometry_subsingleton
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β}
[subsingleton α] :
isometry f
Any map on a subsingleton is an isometry
theorem
isometry.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[emetric_space α]
[emetric_space β]
[emetric_space γ]
{g : β → γ}
{f : α → β} :
The composition of isometries is an isometry
theorem
isometry.uniform_embedding
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β} :
isometry f → uniform_embedding f
An isometry is an embedding
theorem
isometry.continuous
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β} :
isometry f → continuous f
An isometry is continuous.
theorem
isometry.right_inv
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β}
{g : β → α} :
isometry f → function.right_inverse g f → isometry g
The right inverse of an isometry is an isometry.
theorem
isometry.ediam_image
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β}
(hf : isometry f)
(s : set α) :
emetric.diam (f '' s) = emetric.diam s
Isometries preserve the diameter in emetric spaces.
theorem
isometry.ediam_range
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β} :
isometry f → emetric.diam (set.range f) = emetric.diam set.univ
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 α) :
metric.diam (f '' s) = metric.diam s
An isometry preserves the diameter in metric spaces.
theorem
isometry.diam_range
{α : Type u}
{β : Type v}
[metric_space α]
[metric_space β]
{f : α → β} :
isometry f → metric.diam (set.range f) = metric.diam set.univ
structure
isometric
(α : Type u_1)
(β : Type u_2)
[emetric_space α]
[emetric_space β] :
Type (max u_1 u_2)
α and β are isometric if there is an isometric bijection between them.
@[instance]
def
isometric.has_coe_to_fun
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β] :
has_coe_to_fun (α ≃ᵢ β)
theorem
isometric.coe_eq_to_equiv
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β)
(a : α) :
theorem
isometric.isometry
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.edist_eq
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β)
(x y : α) :
has_edist.edist (⇑h x) (⇑h y) = has_edist.edist x y
theorem
isometric.dist_eq
{α : Type u_1}
{β : Type u_2}
[metric_space α]
[metric_space β]
(h : α ≃ᵢ β)
(x y : α) :
has_dist.dist (⇑h x) (⇑h y) = has_dist.dist x y
theorem
isometric.continuous
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.to_equiv_inj
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
⦃h₁ h₂ : α ≃ᵢ β⦄ :
@[ext]
theorem
isometric.ext
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
⦃h₁ h₂ : α ≃ᵢ β⦄ :
def
isometric.mk'
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(f : α → β)
(g : β → α) :
Alternative constructor for isometric bijections, taking as input an isometry, and a right inverse.
Equations
- isometric.mk' f g hfg hf = {to_equiv := {to_fun := f, inv_fun := g, left_inv := _, right_inv := hfg}, isometry_to_fun := hf}
The identity isometry of a space.
Equations
- isometric.refl α = {to_equiv := {to_fun := (equiv.refl α).to_fun, inv_fun := (equiv.refl α).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}
def
isometric.trans
{α : Type u}
{β : Type v}
{γ : Type w}
[emetric_space α]
[emetric_space β]
[emetric_space γ] :
The composition of two isometric isomorphisms, as an isometric isomorphism.
@[simp]
theorem
isometric.trans_apply
{α : Type u}
{β : Type v}
{γ : Type w}
[emetric_space α]
[emetric_space β]
[emetric_space γ]
(h₁ : α ≃ᵢ β)
(h₂ : β ≃ᵢ γ)
(x : α) :
The inverse of an isometric isomorphism, as an isometric isomorphism.
@[simp]
theorem
isometric.symm_symm
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.apply_symm_apply
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β)
(y : β) :
@[simp]
theorem
isometric.symm_apply_apply
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β)
(x : α) :
theorem
isometric.symm_apply_eq
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β)
{x : α}
{y : β} :
theorem
isometric.eq_symm_apply
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β)
{x : α}
{y : β} :
theorem
isometric.symm_comp_self
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.self_comp_symm
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.range_coe
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.image_symm
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.preimage_symm
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.symm_trans_apply
{α : Type u}
{β : Type v}
{γ : Type w}
[emetric_space α]
[emetric_space β]
[emetric_space γ]
(h₁ : α ≃ᵢ β)
(h₂ : β ≃ᵢ γ)
(x : γ) :
The (bundled) homeomorphism associated to an isometric isomorphism.
Equations
- h.to_homeomorph = {to_equiv := h.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
isometric.coe_to_homeomorph
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
⇑(h.to_homeomorph) = ⇑h
@[simp]
theorem
isometric.to_homeomorph_to_equiv
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
(h : α ≃ᵢ β) :
@[instance]
The group of isometries.
Equations
- isometric.group = {mul := λ (e₁ e₂ : α ≃ᵢ α), e₁.trans e₂, mul_assoc := _, one := isometric.refl α _inst_1, one_mul := _, mul_one := _, inv := isometric.symm _inst_1, mul_left_inv := _}
@[simp]
@[simp]
@[simp]
Addition y ↦ y + x as an isometry.
Equations
- isometric.add_right x = {to_equiv := {to_fun := (equiv.add_right x).to_fun, inv_fun := (equiv.add_right x).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}
@[simp]
@[simp]
theorem
isometric.coe_add_right
{G : Type u_1}
[normed_group G]
(x : G) :
⇑(isometric.add_right x) = λ (y : G), y + x
theorem
isometric.add_right_apply
{G : Type u_1}
[normed_group G]
(x y : G) :
⇑(isometric.add_right x) y = y + x
@[simp]
theorem
isometric.add_right_symm
{G : Type u_1}
[normed_group G]
(x : G) :
(isometric.add_right x).symm = isometric.add_right (-x)
Addition y ↦ x + y as an isometry.
Equations
- isometric.add_left x = {to_equiv := equiv.add_left x, isometry_to_fun := _}
@[simp]
@[simp]
theorem
isometric.coe_add_left
{G : Type u_1}
[normed_group G]
(x : G) :
⇑(isometric.add_left x) = has_add.add x
@[simp]
theorem
isometric.add_left_symm
{G : Type u_1}
[normed_group G]
(x : G) :
(isometric.add_left x).symm = isometric.add_left (-x)
Negation x ↦ -x as an isometry.
Equations
- isometric.neg G = {to_equiv := equiv.neg G (add_comm_group.to_add_group G), isometry_to_fun := _}
@[simp]
theorem
isometric.neg_symm
{G : Type u_1}
[normed_group G] :
(isometric.neg G).symm = isometric.neg G
@[simp]
theorem
isometric.neg_to_equiv
{G : Type u_1}
[normed_group G] :
(isometric.neg G).to_equiv = equiv.neg G
@[simp]
def
isometry.isometric_on_range
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β} :
An isometry induces an isometric isomorphism between the source space and the range of the isometry.
Equations
- h.isometric_on_range = {to_equiv := {to_fun := (equiv.set.range f _).to_fun, inv_fun := (equiv.set.range f _).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}
@[simp]
theorem
isometry.isometric_on_range_apply
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{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 𝕜']
[normed_algebra 𝕜 𝕜'] :
isometry ⇑(algebra_map 𝕜 𝕜')
In a normed algebra, the inclusion of the base field in the extended field is an isometry.
In this section, we show that any separable metric space can be embedded isometrically in ℓ^∞(ℝ)
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
- Kuratowski_embedding.embedding_of_subset x a = bounded_continuous_function.of_normed_group_discrete (λ (n : ℕ), has_dist.dist a (x n) - has_dist.dist (x 0) (x n)) (has_dist.dist a (x 0)) _
theorem
Kuratowski_embedding.embedding_of_subset_coe
{α : Type u}
{n : ℕ}
[metric_space α]
(x : ℕ → α)
(a : α) :
⇑(Kuratowski_embedding.embedding_of_subset x a) n = has_dist.dist a (x n) - has_dist.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 α]
[topological_space.separable_space α] :
Every separable metric space embeds isometrically in ℓ_infty_ℝ.
def
Kuratowski_embedding
(α : Type u)
[metric_space α]
[topological_space.separable_space α] :
α → ℓ_infty_ℝ
The Kuratowski embedding is an isometric embedding of a separable metric space in ℓ^∞(ℝ)
Equations
theorem
Kuratowski_embedding.isometry
(α : Type u)
[metric_space α]
[topological_space.separable_space α] :
The Kuratowski embedding is an isometry
def
nonempty_compacts.Kuratowski_embedding
(α : Type u)
[metric_space α]
[compact_space α]
[nonempty α] :
Version of the Kuratowski embedding for nonempty compacts