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.

def Isometry {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (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 : α), edist (f x1) (f x2) = edist x1 x2

theorem isometry_iff_nndist_eq {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = 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} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = 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} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : Isometry f → ∀ (x y : α), dist (f x) (f y) = dist x y

An isometry preserves distances.

theorem Isometry.of_dist_eq {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : (∀ (x y : α), dist (f x) (f y) = dist x y) → Isometry f

A map that preserves distances is an isometry

theorem Isometry.nndist_eq {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : Isometry f → ∀ (x y : α), nndist (f x) (f y) = nndist x y

An isometry preserves non-negative distances.

theorem Isometry.of_nndist_eq {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : (∀ (x y : α), nndist (f x) (f y) = nndist x y) → Isometry f

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

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

An isometry preserves edistances.

theorem Isometry.lipschitz {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) : LipschitzWith 1 f

theorem Isometry.antilipschitz {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) : AntilipschitzWith 1 f

theorem isometry_subsingleton {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} [Subsingleton α] : Isometry f

Any map on a subsingleton is an isometry

theorem isometry_id {α : Type u} [PseudoEMetricSpace α] : Isometry id

The identity is an isometry

theorem Isometry.prod_map {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {δ : Type u_2} [PseudoEMetricSpace δ] {f : α → β} {g : γ → δ} (hf : Isometry f) (hg : Isometry g) : Isometry (Prod.map f g)

theorem Isometry.piMap {ι : Type u_4} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [(i : ι) → PseudoEMetricSpace (α i)] [(i : ι) → PseudoEMetricSpace (β i)] (f : (i : ι) → α i → β i) (hf : ∀ (i : ι), Isometry (f i)) : Isometry (Pi.map f)

@[deprecated Isometry.piMap]

theorem isometry_dcomp {ι : Type u_4} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [(i : ι) → PseudoEMetricSpace (α i)] [(i : ι) → PseudoEMetricSpace (β i)] (f : (i : ι) → α i → β i) (hf : ∀ (i : ι), Isometry (f i)) : Isometry (Pi.map f)

Alias of Isometry.piMap.

theorem Isometry.comp {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β → γ} {f : α → β} (hg : Isometry g) (hf : Isometry f) : Isometry (g ∘ f)

The composition of isometries is an isometry.

theorem Isometry.uniformContinuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : UniformContinuous f

An isometry from a metric space is a uniform continuous map

theorem Isometry.isUniformInducing {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : IsUniformInducing f

An isometry from a metric space is a uniform inducing map

@[deprecated Isometry.isUniformInducing]

theorem Isometry.uniformInducing {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : IsUniformInducing f

Alias of Isometry.isUniformInducing.

---

An isometry from a metric space is a uniform inducing map

theorem Isometry.tendsto_nhds_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {ι : Type u_2} {f : α → β} {g : ι → α} {a : Filter ι} {b : α} (hf : Isometry f) : Filter.Tendsto g a (nhds b) ↔ Filter.Tendsto (f ∘ g) a (nhds (f b))

theorem Isometry.continuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : Continuous f

An isometry is continuous.

theorem Isometry.right_inv {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {g : β → α} (h : Isometry f) (hg : Function.RightInverse g f) : Isometry g

The right inverse of an isometry is an isometry.

theorem Isometry.preimage_emetric_closedBall {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) (x : α) (r : ENNReal) : f ⁻¹' EMetric.closedBall (f x) r = EMetric.closedBall x r

theorem Isometry.preimage_emetric_ball {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {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} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {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} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : EMetric.diam (Set.range f) = EMetric.diam Set.univ

theorem Isometry.mapsTo_emetric_ball {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ENNReal) : Set.MapsTo f (EMetric.ball x r) (EMetric.ball (f x) r)

theorem Isometry.mapsTo_emetric_closedBall {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ENNReal) : Set.MapsTo f (EMetric.closedBall x r) (EMetric.closedBall (f x) r)

theorem isometry_subtype_coe {α : Type u} [PseudoEMetricSpace α] {s : Set α} : Isometry Subtype.val

The injection from a subtype is an isometry

theorem Isometry.comp_continuousOn_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {γ : Type u_2} [TopologicalSpace γ] (hf : Isometry f) {g : γ → α} {s : Set γ} : ContinuousOn (f ∘ g) s ↔ ContinuousOn g s

theorem Isometry.comp_continuous_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {γ : Type u_2} [TopologicalSpace γ] (hf : Isometry f) {g : γ → α} : Continuous (f ∘ g) ↔ Continuous g

theorem Isometry.injective {α : Type u} {β : Type v} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) : Function.Injective f

An isometry from an emetric space is injective

theorem Isometry.isUniformEmbedding {α : Type u} {β : Type v} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : IsUniformEmbedding f

An isometry from an emetric space is a uniform embedding

@[deprecated Isometry.isUniformEmbedding]

theorem Isometry.uniformEmbedding {α : Type u} {β : Type v} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : IsUniformEmbedding f

Alias of Isometry.isUniformEmbedding.

---

An isometry from an emetric space is a uniform embedding

theorem Isometry.isEmbedding {α : Type u} {β : Type v} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : IsEmbedding f

An isometry from an emetric space is an embedding

@[deprecated Isometry.isEmbedding]

theorem Isometry.embedding {α : Type u} {β : Type v} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) : IsEmbedding f

Alias of Isometry.isEmbedding.

---

An isometry from an emetric space is an embedding

theorem Isometry.isClosedEmbedding {α : Type u} {γ : Type w} [EMetricSpace α] [CompleteSpace α] [EMetricSpace γ] {f : α → γ} (hf : Isometry f) : IsClosedEmbedding f

An isometry from a complete emetric space is a closed embedding

@[deprecated Isometry.isClosedEmbedding]

theorem Isometry.closedEmbedding {α : Type u} {γ : Type w} [EMetricSpace α] [CompleteSpace α] [EMetricSpace γ] {f : α → γ} (hf : Isometry f) : IsClosedEmbedding f

Alias of Isometry.isClosedEmbedding.

---

An isometry from a complete emetric space is a closed embedding

theorem Isometry.diam_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {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} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) : Metric.diam (Set.range f) = Metric.diam Set.univ

theorem Isometry.preimage_setOf_dist {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (p : ℝ → Prop) : f ⁻¹' {y : β | p (dist y (f x))} = {y : α | p (dist y x)}

theorem Isometry.preimage_closedBall {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r

theorem Isometry.preimage_ball {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.ball (f x) r = Metric.ball x r

theorem Isometry.preimage_sphere {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r

theorem Isometry.mapsTo_ball {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : Set.MapsTo f (Metric.ball x r) (Metric.ball (f x) r)

theorem Isometry.mapsTo_sphere {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : Set.MapsTo f (Metric.sphere x r) (Metric.sphere (f x) r)

theorem Isometry.mapsTo_closedBall {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ℝ) : Set.MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) r)

theorem IsUniformEmbedding.to_isometry {α : Type u_2} {β : Type u_3} [UniformSpace α] [MetricSpace β] {f : α → β} (h : IsUniformEmbedding 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.

@[deprecated IsUniformEmbedding.to_isometry]

theorem UniformEmbedding.to_isometry {α : Type u_2} {β : Type u_3} [UniformSpace α] [MetricSpace β] {f : α → β} (h : IsUniformEmbedding f) : Isometry f

Alias of IsUniformEmbedding.to_isometry.

---

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 IsEmbedding.to_isometry {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [MetricSpace β] {f : α → β} (h : IsEmbedding 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.

@[deprecated IsEmbedding.to_isometry]

theorem Embedding.to_isometry {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [MetricSpace β] {f : α → β} (h : IsEmbedding f) : Isometry f

Alias of IsEmbedding.to_isometry.

---

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.

structure IsometryEquiv (α : Type u) (β : Type v) [PseudoEMetricSpace α] [PseudoEMetricSpace β] extends Equiv : Type (max u v)

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

• toFun : α → β
• invFun : β → α
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• isometry_toFun : Isometry self.toFun

theorem IsometryEquiv.isometry_toFun {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (self : α ≃ᵢ β) : Isometry self.toFun

def «term_≃ᵢ_» : Lean.TrailingParserDescr

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

Equations

• «term_≃ᵢ_» = Lean.ParserDescr.trailingNode `«term_≃ᵢ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵢ ") (Lean.ParserDescr.cat `term 26))

theorem IsometryEquiv.toEquiv_injective {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : Function.Injective IsometryEquiv.toEquiv

@[simp]

theorem IsometryEquiv.toEquiv_inj {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {e₁ : α ≃ᵢ β} {e₂ : α ≃ᵢ β} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

instance IsometryEquiv.instEquivLike {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : EquivLike (α ≃ᵢ β) α β

Equations

• IsometryEquiv.instEquivLike = { coe := fun (e : α ≃ᵢ β) => ⇑e.toEquiv, inv := fun (e : α ≃ᵢ β) => ⇑e.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

theorem IsometryEquiv.coe_eq_toEquiv {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (a : α) : h a = h.toEquiv a

@[simp]

theorem IsometryEquiv.coe_toEquiv {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : ⇑h.toEquiv = ⇑h

@[simp]

theorem IsometryEquiv.coe_mk {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (e : α ≃ β) (h : Isometry e.toFun) : ⇑{ toEquiv := e, isometry_toFun := h } = ⇑e

theorem IsometryEquiv.isometry {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : Isometry ⇑h

theorem IsometryEquiv.bijective {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : Function.Bijective ⇑h

theorem IsometryEquiv.injective {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : Function.Injective ⇑h

theorem IsometryEquiv.surjective {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : Function.Surjective ⇑h

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

theorem IsometryEquiv.dist_eq {α : Type u_2} {β : Type u_3} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (y : α) : dist (h x) (h y) = dist x y

theorem IsometryEquiv.nndist_eq {α : Type u_2} {β : Type u_3} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (y : α) : nndist (h x) (h y) = nndist x y

theorem IsometryEquiv.continuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : Continuous ⇑h

@[simp]

theorem IsometryEquiv.ediam_image {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (s : Set α) : EMetric.diam (⇑h '' s) = EMetric.diam s

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

def IsometryEquiv.mk' {β : Type v} [PseudoEMetricSpace β] {α : Type u} [EMetricSpace α] (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

• IsometryEquiv.mk' f g hfg hf = { toFun := f, invFun := g, left_inv := ⋯, right_inv := hfg, isometry_toFun := hf }

def IsometryEquiv.refl (α : Type u_2) [PseudoEMetricSpace α] : α ≃ᵢ α

The identity isometry of a space.

Equations

• IsometryEquiv.refl α = { toEquiv := Equiv.refl α, isometry_toFun := ⋯ }

def IsometryEquiv.trans {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) : α ≃ᵢ γ

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

Equations

• h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, isometry_toFun := ⋯ }

@[simp]

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

def IsometryEquiv.symm {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : β ≃ᵢ α

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

Equations

• h.symm = { toEquiv := h.symm, isometry_toFun := ⋯ }

def IsometryEquiv.Simps.apply {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (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

• IsometryEquiv.Simps.apply h = ⇑h

def IsometryEquiv.Simps.symm_apply {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : β → α

See Note [custom simps projection]

Equations

• IsometryEquiv.Simps.symm_apply h = ⇑h.symm

@[simp]

theorem IsometryEquiv.symm_symm {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : h.symm.symm = h

theorem IsometryEquiv.symm_bijective {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : Function.Bijective IsometryEquiv.symm

@[simp]

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

@[simp]

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

theorem IsometryEquiv.symm_apply_eq {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) {x : α} {y : β} : h.symm y = x ↔ y = h x

theorem IsometryEquiv.eq_symm_apply {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) {x : α} {y : β} : x = h.symm y ↔ h x = y

theorem IsometryEquiv.symm_comp_self {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : ⇑h.symm ∘ ⇑h = id

theorem IsometryEquiv.self_comp_symm {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : ⇑h ∘ ⇑h.symm = id

@[simp]

theorem IsometryEquiv.range_eq_univ {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : Set.range ⇑h = Set.univ

theorem IsometryEquiv.image_symm {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : Set.image ⇑h.symm = Set.preimage ⇑h

theorem IsometryEquiv.preimage_symm {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : Set.preimage ⇑h.symm = Set.image ⇑h

@[simp]

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

theorem IsometryEquiv.ediam_univ {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : EMetric.diam Set.univ = EMetric.diam Set.univ

@[simp]

theorem IsometryEquiv.ediam_preimage {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (s : Set β) : EMetric.diam (⇑h ⁻¹' s) = EMetric.diam s

@[simp]

theorem IsometryEquiv.preimage_emetric_ball {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ENNReal) : ⇑h ⁻¹' EMetric.ball x r = EMetric.ball (h.symm x) r

@[simp]

theorem IsometryEquiv.preimage_emetric_closedBall {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ENNReal) : ⇑h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (h.symm x) r

@[simp]

theorem IsometryEquiv.image_emetric_ball {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ENNReal) : ⇑h '' EMetric.ball x r = EMetric.ball (h x) r

@[simp]

theorem IsometryEquiv.image_emetric_closedBall {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ENNReal) : ⇑h '' EMetric.closedBall x r = EMetric.closedBall (h x) r

def IsometryEquiv.toHomeomorph {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : α ≃ₜ β

The (bundled) homeomorphism associated to an isometric isomorphism.

Equations

• h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem IsometryEquiv.toHomeomorph_toEquiv {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : h.toHomeomorph.toEquiv = h.toEquiv

@[simp]

theorem IsometryEquiv.coe_toHomeomorph {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : ⇑h.toHomeomorph = ⇑h

@[simp]

theorem IsometryEquiv.coe_toHomeomorph_symm {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) : ⇑h.toHomeomorph.symm = ⇑h.symm

@[simp]

theorem IsometryEquiv.comp_continuousOn_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {γ : Type u_2} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α} {s : Set γ} : ContinuousOn (⇑h ∘ f) s ↔ ContinuousOn f s

@[simp]

theorem IsometryEquiv.comp_continuous_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {γ : Type u_2} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α} : Continuous (⇑h ∘ f) ↔ Continuous f

@[simp]

theorem IsometryEquiv.comp_continuous_iff' {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {γ : Type u_2} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : β → γ} : Continuous (f ∘ ⇑h) ↔ Continuous f

instance IsometryEquiv.instGroup {α : Type u} [PseudoEMetricSpace α] : Group (α ≃ᵢ α)

The group of isometries.

Equations

• IsometryEquiv.instGroup = Group.mk ⋯

@[simp]

theorem IsometryEquiv.coe_one {α : Type u} [PseudoEMetricSpace α] : ⇑1 = id

@[simp]

theorem IsometryEquiv.coe_mul {α : Type u} [PseudoEMetricSpace α] (e₁ : α ≃ᵢ α) (e₂ : α ≃ᵢ α) : ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

theorem IsometryEquiv.mul_apply {α : Type u} [PseudoEMetricSpace α] (e₁ : α ≃ᵢ α) (e₂ : α ≃ᵢ α) (x : α) : (e₁ * e₂) x = e₁ (e₂ x)

@[simp]

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

@[simp]

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

theorem IsometryEquiv.completeSpace_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (e : α ≃ᵢ β) : CompleteSpace α ↔ CompleteSpace β

theorem IsometryEquiv.completeSpace {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [CompleteSpace β] (e : α ≃ᵢ β) : CompleteSpace α

def IsometryEquiv.piCongrLeft' {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι → Type u_3} [(j : ι) → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : ((i : ι) → Y i) ≃ᵢ ((j : ι') → Y (e.symm j))

The natural isometry ∀ i, Y i ≃ᵢ ∀ j, Y (e.symm j) obtained from a bijection ι ≃ ι' of fintypes. Equiv.piCongrLeft' as an IsometryEquiv.

Equations

• IsometryEquiv.piCongrLeft' e = { toEquiv := Equiv.piCongrLeft' Y e, isometry_toFun := ⋯ }

@[simp]

theorem IsometryEquiv.piCongrLeft'_symm_apply {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι → Type u_3} [(j : ι) → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (f : (b : ι') → Y (e.symm b)) (x : ι) : (IsometryEquiv.piCongrLeft' e).symm f x = ⋯ ▸ f (e x)

@[simp]

theorem IsometryEquiv.piCongrLeft'_toFun {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι → Type u_3} [(j : ι) → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (f : (a : ι) → Y a) (x : ι') : (IsometryEquiv.piCongrLeft' e) f x = f (e.symm x)

@[simp]

theorem IsometryEquiv.piCongrLeft'_apply {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι → Type u_3} [(j : ι) → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (f : (a : ι) → Y a) (x : ι') : (IsometryEquiv.piCongrLeft' e) f x = f (e.symm x)

@[simp]

theorem IsometryEquiv.piCongrLeft'_invFun {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι → Type u_3} [(j : ι) → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (f : (b : ι') → Y (e.symm b)) (x : ι) : (IsometryEquiv.piCongrLeft' e).invFun f x = ⋯ ▸ f (e x)

def IsometryEquiv.piCongrLeft {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι' → Type u_3} [(j : ι') → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : ((i : ι) → Y (e i)) ≃ᵢ ((j : ι') → Y j)

The natural isometry ∀ i, Y (e i) ≃ᵢ ∀ j, Y j obtained from a bijection ι ≃ ι' of fintypes. Equiv.piCongrLeft as an IsometryEquiv.

Equations

• IsometryEquiv.piCongrLeft e = (IsometryEquiv.piCongrLeft' e.symm).symm

@[simp]

theorem IsometryEquiv.piCongrLeft_apply {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι' → Type u_3} [(j : ι') → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : ∀ (a : (j : ι) → Y (e.symm.symm j)) (i : ι'), (IsometryEquiv.piCongrLeft e) a i = ⋯ ▸ a (e.symm i)

@[simp]

theorem IsometryEquiv.piCongrLeft_symm_apply {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι' → Type u_3} [(j : ι') → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : ∀ (a : (i : ι') → Y i) (j : ι), (IsometryEquiv.piCongrLeft e).symm a j = (IsometryEquiv.piCongrLeft' e.symm) a j

@[simp]

theorem IsometryEquiv.piCongrLeft_invFun {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι' → Type u_3} [(j : ι') → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : ∀ (a : (i : ι') → Y i) (j : ι), (IsometryEquiv.piCongrLeft e).invFun a j = (IsometryEquiv.piCongrLeft' e.symm) a j

@[simp]

theorem IsometryEquiv.piCongrLeft_toFun {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {Y : ι' → Type u_3} [(j : ι') → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : ∀ (a : (j : ι) → Y (e.symm.symm j)) (i : ι'), (IsometryEquiv.piCongrLeft e) a i = ⋯ ▸ a (e.symm i)

def IsometryEquiv.sumArrowIsometryEquivProdArrow {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace γ] [Fintype α] [Fintype β] : (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)

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.

Equations

• IsometryEquiv.sumArrowIsometryEquivProdArrow = { toEquiv := Equiv.sumArrowEquivProdArrow α β γ, isometry_toFun := ⋯ }

@[simp]

theorem IsometryEquiv.sumArrowIsometryEquivProdArrow_symm_apply {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace γ] [Fintype α] [Fintype β] (p : (α → γ) × (β → γ)) : ∀ (a : α ⊕ β), IsometryEquiv.sumArrowIsometryEquivProdArrow.symm p a = Sum.elim p.1 p.2 a

@[simp]

theorem IsometryEquiv.sumArrowIsometryEquivProdArrow_invFun {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace γ] [Fintype α] [Fintype β] (p : (α → γ) × (β → γ)) : ∀ (a : α ⊕ β), IsometryEquiv.sumArrowIsometryEquivProdArrow.invFun p a = Sum.elim p.1 p.2 a

@[simp]

theorem IsometryEquiv.sumArrowIsometryEquivProdArrow_toFun {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace γ] [Fintype α] [Fintype β] (f : α ⊕ β → γ) : IsometryEquiv.sumArrowIsometryEquivProdArrow f = (f ∘ Sum.inl, f ∘ Sum.inr)

@[simp]

theorem IsometryEquiv.sumArrowIsometryEquivProdArrow_apply {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace γ] [Fintype α] [Fintype β] (f : α ⊕ β → γ) : IsometryEquiv.sumArrowIsometryEquivProdArrow f = (f ∘ Sum.inl, f ∘ Sum.inr)

@[simp]

theorem IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph {γ : Type w} [PseudoEMetricSpace γ] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] : IsometryEquiv.sumArrowIsometryEquivProdArrow.toHomeomorph = Homeomorph.sumArrowHomeomorphProdArrow

theorem Fin.edist_append_eq_max_edist {α : Type u} [PseudoEMetricSpace α] (m : ℕ) (n : ℕ) {x : Fin m → α} {x2 : Fin m → α} {y : Fin n → α} {y2 : Fin n → α} : edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2)

def Fin.appendIsometry {α : Type u} [PseudoEMetricSpace α] (m : ℕ) (n : ℕ) : (Fin m → α) × (Fin n → α) ≃ᵢ (Fin (m + n) → α)

The natural IsometryEquiv between (Fin m → α) × (Fin n → α) and Fin (m + n) → α. Fin.appendEquiv as an IsometryEquiv.

Equations

• Fin.appendIsometry m n = { toEquiv := Fin.appendEquiv m n, isometry_toFun := ⋯ }

@[simp]

theorem Fin.appendIsometry_toFun {α : Type u} [PseudoEMetricSpace α] (m : ℕ) (n : ℕ) (fg : (Fin m → α) × (Fin n → α)) : ∀ (a : Fin (m + n)), (Fin.appendIsometry m n) fg a = Fin.append fg.1 fg.2 a

@[simp]

theorem Fin.appendIsometry_apply {α : Type u} [PseudoEMetricSpace α] (m : ℕ) (n : ℕ) (fg : (Fin m → α) × (Fin n → α)) : ∀ (a : Fin (m + n)), (Fin.appendIsometry m n) fg a = Fin.append fg.1 fg.2 a

@[simp]

theorem Fin.appendIsometry_symm_apply {α : Type u} [PseudoEMetricSpace α] (m : ℕ) (n : ℕ) (f : Fin (m + n) → α) : (Fin.appendIsometry m n).symm f = (fun (i : Fin m) => f (Fin.castAdd n i), fun (i : Fin n) => f (Fin.natAdd m i))

@[simp]

theorem Fin.appendIsometry_invFun {α : Type u} [PseudoEMetricSpace α] (m : ℕ) (n : ℕ) (f : Fin (m + n) → α) : (Fin.appendIsometry m n).invFun f = (fun (i : Fin m) => f (Fin.castAdd n i), fun (i : Fin n) => f (Fin.natAdd m i))

@[simp]

theorem Fin.appendIsometry_toHomeomorph {α : Type u} [PseudoEMetricSpace α] (m : ℕ) (n : ℕ) : (Fin.appendIsometry m n).toHomeomorph = Fin.appendHomeomorph m n

def IsometryEquiv.funUnique (ι : Type u_1) (α : Type u) [PseudoEMetricSpace α] [Unique ι] [Fintype ι] : (ι → α) ≃ᵢ α

Equiv.funUnique as an IsometryEquiv.

Equations

• IsometryEquiv.funUnique ι α = { toEquiv := Equiv.funUnique ι α, isometry_toFun := ⋯ }

@[simp]

theorem IsometryEquiv.funUnique_invFun (ι : Type u_1) (α : Type u) [PseudoEMetricSpace α] [Unique ι] [Fintype ι] (x : α) (i : ι) : (IsometryEquiv.funUnique ι α).invFun x i = x

@[simp]

theorem IsometryEquiv.funUnique_apply (ι : Type u_1) (α : Type u) [PseudoEMetricSpace α] [Unique ι] [Fintype ι] (f : (i : ι) → (fun (a : ι) => α) i) : (IsometryEquiv.funUnique ι α) f = f default

@[simp]

theorem IsometryEquiv.funUnique_toFun (ι : Type u_1) (α : Type u) [PseudoEMetricSpace α] [Unique ι] [Fintype ι] (f : (i : ι) → (fun (a : ι) => α) i) : (IsometryEquiv.funUnique ι α) f = f default

@[simp]

theorem IsometryEquiv.funUnique_symm_apply (ι : Type u_1) (α : Type u) [PseudoEMetricSpace α] [Unique ι] [Fintype ι] (x : α) (i : ι) : (IsometryEquiv.funUnique ι α).symm x i = x

def IsometryEquiv.piFinTwo (α : Fin 2 → Type u_2) [(i : Fin 2) → PseudoEMetricSpace (α i)] : ((i : Fin 2) → α i) ≃ᵢ α 0 × α 1

piFinTwoEquiv as an IsometryEquiv.

Equations

• IsometryEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, isometry_toFun := ⋯ }

@[simp]

theorem IsometryEquiv.piFinTwo_invFun (α : Fin 2 → Type u_2) [(i : Fin 2) → PseudoEMetricSpace (α i)] (p : α 0 × α 1) (i : Fin (1 + 1)) : (IsometryEquiv.piFinTwo α).invFun p i = Fin.cons p.1 (Fin.cons p.2 finZeroElim) i

@[simp]

theorem IsometryEquiv.piFinTwo_apply (α : Fin 2 → Type u_2) [(i : Fin 2) → PseudoEMetricSpace (α i)] (f : (i : Fin 2) → α i) : (IsometryEquiv.piFinTwo α) f = (f 0, f 1)

@[simp]

theorem IsometryEquiv.piFinTwo_toFun (α : Fin 2 → Type u_2) [(i : Fin 2) → PseudoEMetricSpace (α i)] (f : (i : Fin 2) → α i) : (IsometryEquiv.piFinTwo α) f = (f 0, f 1)

@[simp]

theorem IsometryEquiv.piFinTwo_symm_apply (α : Fin 2 → Type u_2) [(i : Fin 2) → PseudoEMetricSpace (α i)] (p : α 0 × α 1) (i : Fin (1 + 1)) : (IsometryEquiv.piFinTwo α).symm p i = Fin.cons p.1 (Fin.cons p.2 finZeroElim) i

@[simp]

theorem IsometryEquiv.diam_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (s : Set α) : Metric.diam (⇑h '' s) = Metric.diam s

@[simp]

theorem IsometryEquiv.diam_preimage {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (s : Set β) : Metric.diam (⇑h ⁻¹' s) = Metric.diam s

theorem IsometryEquiv.diam_univ {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) : Metric.diam Set.univ = Metric.diam Set.univ

@[simp]

theorem IsometryEquiv.preimage_ball {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ) : ⇑h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r

@[simp]

theorem IsometryEquiv.preimage_sphere {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ) : ⇑h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r

@[simp]

theorem IsometryEquiv.preimage_closedBall {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ) : ⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r

@[simp]

theorem IsometryEquiv.image_ball {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ) : ⇑h '' Metric.ball x r = Metric.ball (h x) r

@[simp]

theorem IsometryEquiv.image_sphere {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ) : ⇑h '' Metric.sphere x r = Metric.sphere (h x) r

@[simp]

theorem IsometryEquiv.image_closedBall {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ) : ⇑h '' Metric.closedBall x r = Metric.closedBall (h x) r

def Isometry.isometryEquivOnRange {α : Type u} {β : Type v} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) : α ≃ᵢ ↑(Set.range f)

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

Equations

• h.isometryEquivOnRange = { toEquiv := Equiv.ofInjective f ⋯, isometry_toFun := h }

@[simp]

theorem Isometry.isometryEquivOnRange_toEquiv {α : Type u} {β : Type v} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) : h.isometryEquivOnRange.toEquiv = Equiv.ofInjective f ⋯

@[simp]

theorem Isometry.isometryEquivOnRange_apply {α : Type u} {β : Type v} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) (a : α) : h.isometryEquivOnRange a = ⟨f a, ⋯⟩

theorem Isometry.lipschitzWith_iff {α : Type u_2} {β : Type u_3} {γ : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : α → β} {g : β → γ} (K : NNReal) (h : Isometry g) : LipschitzWith K (g ∘ f) ↔ LipschitzWith K f

Post-composition by an isometry does not change the Lipschitz-property of a function.