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 pseudo_metric_space and we specialize to metric_space when needed.
def
isometry
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(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
- isometry f = ∀ (x1 x2 : α), has_edist.edist (f x1) (f x2) = has_edist.edist x1 x2
theorem
isometry_iff_nndist_eq
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
isometry f ↔ ∀ (x y : α), has_nndist.nndist (f x) (f y) = has_nndist.nndist x 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}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
isometry f ↔ ∀ (x y : α), has_dist.dist (f x) (f y) = has_dist.dist x y
On pseudometric spaces, a map is an isometry if and only if it preserves distances.
theorem
isometry.dist_eq
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
isometry f → ∀ (x y : α), has_dist.dist (f x) (f y) = has_dist.dist x y
An isometry preserves distances.
theorem
isometry.of_dist_eq
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
(∀ (x y : α), has_dist.dist (f x) (f y) = has_dist.dist x y) → isometry f
A map that preserves distances is an isometry
theorem
isometry.nndist_eq
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
isometry f → ∀ (x y : α), has_nndist.nndist (f x) (f y) = has_nndist.nndist x y
An isometry preserves non-negative distances.
theorem
isometry.of_nndist_eq
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
(∀ (x y : α), has_nndist.nndist (f x) (f y) = has_nndist.nndist x y) → isometry f
A map that preserves non-negative distances is an isometry.
theorem
isometry.edist_eq
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_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.lipschitz
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : isometry f) :
lipschitz_with 1 f
theorem
isometry.antilipschitz
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : isometry f) :
theorem
isometry_subsingleton
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
[subsingleton α] :
isometry f
Any map on a subsingleton is an isometry
The identity is an isometry
theorem
isometry.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
{g : β → γ}
{f : α → β}
(hg : isometry g)
(hf : isometry f) :
The composition of isometries is an isometry
@[protected]
theorem
isometry.uniform_continuous
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f) :
An isometry from a metric space is a uniform continuous map
@[protected]
theorem
isometry.uniform_inducing
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f) :
An isometry from a metric space is a uniform inducing map
theorem
isometry.tendsto_nhds_iff
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{ι : Type u_1}
{f : α → β}
{g : ι → α}
{a : filter ι}
{b : α}
(hf : isometry f) :
filter.tendsto g a (nhds b) ↔ filter.tendsto (f ∘ g) a (nhds (f b))
@[protected]
theorem
isometry.continuous
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f) :
An isometry is continuous.
theorem
isometry.right_inv
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
{g : β → α}
(h : isometry f)
(hg : function.right_inverse g f) :
isometry g
The right inverse of an isometry is an isometry.
theorem
isometry.preimage_emetric_closed_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : isometry f)
(x : α)
(r : ennreal) :
f ⁻¹' emetric.closed_ball (f x) r = emetric.closed_ball x r
theorem
isometry.preimage_emetric_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : isometry f)
(x : α)
(r : ennreal) :
f ⁻¹' emetric.ball (f x) r = emetric.ball x r
theorem
isometry.ediam_image
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f)
(s : set α) :
emetric.diam (f '' s) = emetric.diam s
Isometries preserve the diameter in pseudoemetric spaces.
theorem
isometry.ediam_range
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f) :
theorem
isometry.maps_to_emetric_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(r : ennreal) :
set.maps_to f (emetric.ball x r) (emetric.ball (f x) r)
theorem
isometry.maps_to_emetric_closed_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(r : ennreal) :
set.maps_to f (emetric.closed_ball x r) (emetric.closed_ball (f x) r)
The injection from a subtype is an isometry
theorem
isometry.comp_continuous_on_iff
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
{γ : Type u_1}
[topological_space γ]
(hf : isometry f)
{g : γ → α}
{s : set γ} :
continuous_on (f ∘ g) s ↔ continuous_on g s
theorem
isometry.comp_continuous_iff
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
{γ : Type u_1}
[topological_space γ]
(hf : isometry f)
{g : γ → α} :
continuous (f ∘ g) ↔ continuous g
@[protected]
theorem
isometry.injective
{α : Type u}
{β : Type v}
[emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : isometry f) :
An isometry from an emetric space is injective
@[protected]
theorem
isometry.uniform_embedding
{α : Type u}
{β : Type v}
[emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f) :
An isometry from an emetric space is a uniform embedding
@[protected]
theorem
isometry.embedding
{α : Type u}
{β : Type v}
[emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(hf : isometry f) :
An isometry from an emetric space is an embedding
theorem
isometry.closed_embedding
{α : Type u}
{γ : Type w}
[emetric_space α]
[complete_space α]
[emetric_space γ]
{f : α → γ}
(hf : isometry f) :
An isometry from a complete emetric space is a closed embedding
theorem
isometry.diam_image
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f)
(s : set α) :
metric.diam (f '' s) = metric.diam s
An isometry preserves the diameter in pseudometric spaces.
theorem
isometry.diam_range
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f) :
theorem
isometry.preimage_set_of_dist
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(p : ℝ → Prop) :
f ⁻¹' {y : β | p (has_dist.dist y (f x))} = {y : α | p (has_dist.dist y x)}
theorem
isometry.preimage_closed_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(r : ℝ) :
f ⁻¹' metric.closed_ball (f x) r = metric.closed_ball x r
theorem
isometry.preimage_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(r : ℝ) :
f ⁻¹' metric.ball (f x) r = metric.ball x r
theorem
isometry.preimage_sphere
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(r : ℝ) :
f ⁻¹' metric.sphere (f x) r = metric.sphere x r
theorem
isometry.maps_to_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(r : ℝ) :
set.maps_to f (metric.ball x r) (metric.ball (f x) r)
theorem
isometry.maps_to_sphere
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(r : ℝ) :
set.maps_to f (metric.sphere x r) (metric.sphere (f x) r)
theorem
isometry.maps_to_closed_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : isometry f)
(x : α)
(r : ℝ) :
set.maps_to f (metric.closed_ball x r) (metric.closed_ball (f x) r)
theorem
uniform_embedding.to_isometry
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[metric_space β]
{f : α → β}
(h : uniform_embedding f) :
isometry 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}
[topological_space α]
[metric_space β]
{f : α → β}
(h : embedding f) :
isometry 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
isometric
(α : Type u_1)
(β : Type u_2)
[pseudo_emetric_space α]
[pseudo_emetric_space β] :
Type (max u_1 u_2)
α and β are isometric if there is an isometric bijection between them.
Instances for isometric
- isometric.has_sizeof_inst
- isometric.has_coe_to_fun
- isometric.group
@[protected, instance]
def
isometric.has_coe_to_fun
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β] :
has_coe_to_fun (α ≃ᵢ β) (λ (_x : α ≃ᵢ β), α → β)
theorem
isometric.coe_eq_to_equiv
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(a : α) :
@[simp]
theorem
isometric.coe_to_equiv
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[protected]
theorem
isometric.isometry
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[protected]
theorem
isometric.bijective
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[protected]
theorem
isometric.injective
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[protected]
theorem
isometric.surjective
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[protected]
theorem
isometric.edist_eq
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(x y : α) :
has_edist.edist (⇑h x) (⇑h y) = has_edist.edist x y
@[protected]
theorem
isometric.dist_eq
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(x y : α) :
has_dist.dist (⇑h x) (⇑h y) = has_dist.dist x y
@[protected]
theorem
isometric.nndist_eq
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(x y : α) :
has_nndist.nndist (⇑h x) (⇑h y) = has_nndist.nndist x y
@[protected]
theorem
isometric.continuous
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.ediam_image
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(s : set α) :
emetric.diam (⇑h '' s) = emetric.diam s
theorem
isometric.to_equiv_inj
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
⦃h₁ h₂ : α ≃ᵢ β⦄ :
@[ext]
theorem
isometric.ext
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
⦃h₁ h₂ : α ≃ᵢ β⦄
(H : ∀ (x : α), ⇑h₁ x = ⇑h₂ x) :
h₁ = h₂
def
isometric.mk'
{β : Type v}
[pseudo_emetric_space β]
{α : Type u}
[emetric_space α]
(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
- isometric.mk' f g hfg hf = {to_equiv := {to_fun := f, inv_fun := g, left_inv := _, right_inv := hfg}, isometry_to_fun := hf}
@[protected]
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 := _}
@[protected]
def
isometric.trans
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
(h₁ : α ≃ᵢ β)
(h₂ : β ≃ᵢ γ) :
α ≃ᵢ γ
The composition of two isometric isomorphisms, as an isometric isomorphism.
@[simp]
theorem
isometric.trans_apply
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
(h₁ : α ≃ᵢ β)
(h₂ : β ≃ᵢ γ)
(x : α) :
@[protected]
def
isometric.symm
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
β ≃ᵢ α
The inverse of an isometric isomorphism, as an isometric isomorphism.
def
isometric.simps.apply
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(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
isometric.simps.symm_apply
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
β → α
See Note [custom simps projection]
Equations
- isometric.simps.symm_apply h = ⇑(h.symm)
@[simp]
theorem
isometric.symm_symm
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.apply_symm_apply
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(y : β) :
@[simp]
theorem
isometric.symm_apply_apply
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(x : α) :
theorem
isometric.symm_apply_eq
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
{x : α}
{y : β} :
theorem
isometric.eq_symm_apply
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
{x : α}
{y : β} :
theorem
isometric.symm_comp_self
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.self_comp_symm
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.range_eq_univ
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.image_symm
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
theorem
isometric.preimage_symm
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.symm_trans_apply
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
(h₁ : α ≃ᵢ β)
(h₂ : β ≃ᵢ γ)
(x : γ) :
theorem
isometric.ediam_univ
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.ediam_preimage
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(s : set β) :
emetric.diam (⇑h ⁻¹' s) = emetric.diam s
@[simp]
theorem
isometric.preimage_emetric_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(x : β)
(r : ennreal) :
⇑h ⁻¹' emetric.ball x r = emetric.ball (⇑(h.symm) x) r
@[simp]
theorem
isometric.preimage_emetric_closed_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(x : β)
(r : ennreal) :
⇑h ⁻¹' emetric.closed_ball x r = emetric.closed_ball (⇑(h.symm) x) r
@[simp]
theorem
isometric.image_emetric_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(x : α)
(r : ennreal) :
⇑h '' emetric.ball x r = emetric.ball (⇑h x) r
@[simp]
theorem
isometric.image_emetric_closed_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β)
(x : α)
(r : ennreal) :
⇑h '' emetric.closed_ball x r = emetric.closed_ball (⇑h x) r
@[simp]
theorem
isometric.to_homeomorph_to_equiv
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[protected]
def
isometric.to_homeomorph
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
α ≃ₜ β
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}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
⇑(h.to_homeomorph) = ⇑h
@[simp]
theorem
isometric.coe_to_homeomorph_symm
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.comp_continuous_on_iff
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{γ : Type u_1}
[topological_space γ]
(h : α ≃ᵢ β)
{f : γ → α}
{s : set γ} :
continuous_on (⇑h ∘ f) s ↔ continuous_on f s
@[simp]
theorem
isometric.comp_continuous_iff
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{γ : Type u_1}
[topological_space γ]
(h : α ≃ᵢ β)
{f : γ → α} :
continuous (⇑h ∘ f) ↔ continuous f
@[simp]
theorem
isometric.comp_continuous_iff'
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{γ : Type u_1}
[topological_space γ]
(h : α ≃ᵢ β)
{f : β → γ} :
continuous (f ∘ ⇑h) ↔ continuous f
@[protected, 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 := _, npow := div_inv_monoid.npow._default (isometric.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_4 isometric.group._proof_5, npow_zero' := _, npow_succ' := _, inv := isometric.symm _inst_1, div := div_inv_monoid.div._default (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_8 (isometric.refl α) isometric.group._proof_9 isometric.group._proof_10 (div_inv_monoid.npow._default (isometric.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_4 isometric.group._proof_5) isometric.group._proof_11 isometric.group._proof_12 isometric.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_14 (isometric.refl α) isometric.group._proof_15 isometric.group._proof_16 (div_inv_monoid.npow._default (isometric.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_4 isometric.group._proof_5) isometric.group._proof_17 isometric.group._proof_18 isometric.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
@[simp]
@[simp]
@[protected]
theorem
isometric.complete_space
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[complete_space β]
(e : α ≃ᵢ β) :
theorem
isometric.complete_space_iff
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(e : α ≃ᵢ β) :
@[simp]
theorem
isometric.diam_image
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(s : set α) :
metric.diam (⇑h '' s) = metric.diam s
@[simp]
theorem
isometric.diam_preimage
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(s : set β) :
metric.diam (⇑h ⁻¹' s) = metric.diam s
theorem
isometric.diam_univ
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β) :
@[simp]
theorem
isometric.preimage_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(x : β)
(r : ℝ) :
⇑h ⁻¹' metric.ball x r = metric.ball (⇑(h.symm) x) r
@[simp]
theorem
isometric.preimage_sphere
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(x : β)
(r : ℝ) :
⇑h ⁻¹' metric.sphere x r = metric.sphere (⇑(h.symm) x) r
@[simp]
theorem
isometric.preimage_closed_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(x : β)
(r : ℝ) :
⇑h ⁻¹' metric.closed_ball x r = metric.closed_ball (⇑(h.symm) x) r
@[simp]
theorem
isometric.image_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(x : α)
(r : ℝ) :
⇑h '' metric.ball x r = metric.ball (⇑h x) r
@[simp]
theorem
isometric.image_sphere
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(x : α)
(r : ℝ) :
⇑h '' metric.sphere x r = metric.sphere (⇑h x) r
@[simp]
theorem
isometric.image_closed_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(h : α ≃ᵢ β)
(x : α)
(r : ℝ) :
⇑h '' metric.closed_ball x r = metric.closed_ball (⇑h x) r
noncomputable
def
isometry.isometric_on_range
{α : Type u}
{β : Type v}
[emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : isometry f) :
An isometry induces an isometric isomorphism between the source space and the range of the isometry.
Equations
- h.isometric_on_range = {to_equiv := equiv.of_injective f _, isometry_to_fun := _}
@[simp]
theorem
isometry.isometric_on_range_apply
{α : Type u}
{β : Type v}
[emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : isometry f)
(a : α) :
⇑(h.isometric_on_range) a = ⟨f a, _⟩
@[simp]
theorem
isometry.isometric_on_range_to_equiv
{α : Type u}
{β : Type v}
[emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : isometry f) :