topology.metric_space.isometry

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

source

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.

source

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.

source

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.

source

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

source

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.

source

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.

source

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.

source

theorem isometry.lipschitz {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} (h : isometry f) :

lipschitz_with 1 f

source

theorem isometry.antilipschitz {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} (h : isometry f) :

antilipschitz_with 1 f

source

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

source

theorem isometry_id {α : Type u} [pseudo_emetric_space α] :

isometry id

The identity is an isometry

source

theorem isometry.prod_map {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {δ : Type u_1} [pseudo_emetric_space δ] {f : α → β} {g : γ → δ} (hf : isometry f) (hg : isometry g) :

isometry (prod.map f g)

source

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)) :

isometry (function.dcomp f)

source

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) :

isometry (g ∘ f)

The composition of isometries is an isometry.

source

@[protected]

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

uniform_continuous f

An isometry from a metric space is a uniform continuous map

source

@[protected]

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

uniform_inducing f

An isometry from a metric space is a uniform inducing map

source

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))

source

@[protected]

theorem isometry.continuous {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} (hf : isometry f) :

continuous f

An isometry is continuous.

source

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.

source

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

source

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

source

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.

source

theorem isometry.ediam_range {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} (hf : isometry f) :

emetric.diam (set.range f) = emetric.diam set.univ

source

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)

source

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)

source

theorem isometry_subtype_coe {α : Type u} [pseudo_emetric_space α] {s : set α} :

isometry coe

The injection from a subtype is an isometry

source

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

source

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

source

@[protected]

theorem isometry.injective {α : Type u} {β : Type v} [emetric_space α] [pseudo_emetric_space β] {f : α → β} (h : isometry f) :

function.injective f

An isometry from an emetric space is injective

source

@[protected]

theorem isometry.uniform_embedding {α : Type u} {β : Type v} [emetric_space α] [pseudo_emetric_space β] {f : α → β} (hf : isometry f) :

uniform_embedding f

An isometry from an emetric space is a uniform embedding

source

@[protected]

theorem isometry.embedding {α : Type u} {β : Type v} [emetric_space α] [pseudo_emetric_space β] {f : α → β} (hf : isometry f) :

embedding f

An isometry from an emetric space is an embedding

source

theorem isometry.closed_embedding {α : Type u} {γ : Type w} [emetric_space α] [complete_space α] [emetric_space γ] {f : α → γ} (hf : isometry f) :

closed_embedding f

An isometry from a complete emetric space is a closed embedding

source

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.

source

theorem isometry.diam_range {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} (hf : isometry f) :

metric.diam (set.range f) = metric.diam set.univ

source

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)}

source

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

source

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

source

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

source

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)

source

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)

source

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)

source

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.

source

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.

source

@[nolint]

structure isometry_equiv (α : Type u_2) (β : Type u_3) [pseudo_emetric_space α] [pseudo_emetric_space β] :

Type (max u_2 u_3)

to_equiv : α ≃ β
isometry_to_fun : isometry self.to_equiv.to_fun

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

Instances for isometry_equiv

isometry_equiv.has_sizeof_inst
isometry_equiv.has_coe_to_fun
isometry_equiv.group

source

@[protected, instance]

def isometry_equiv.has_coe_to_fun {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] :

has_coe_to_fun (α ≃ᵢ β) (λ (_x : α ≃ᵢ β), α → β)

Equations

isometry_equiv.has_coe_to_fun = {coe := λ (e : α ≃ᵢ β), ⇑(e.to_equiv)}

source

theorem isometry_equiv.coe_eq_to_equiv {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) (a : α) :

⇑h a = ⇑(h.to_equiv) a

source

@[simp]

theorem isometry_equiv.coe_to_equiv {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

⇑(h.to_equiv) = ⇑h

source

@[protected]

theorem isometry_equiv.isometry {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

isometry ⇑h

source

@[protected]

theorem isometry_equiv.bijective {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

function.bijective ⇑h

source

@[protected]

theorem isometry_equiv.injective {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

function.injective ⇑h

source

@[protected]

theorem isometry_equiv.surjective {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

function.surjective ⇑h

source

@[protected]

theorem isometry_equiv.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

source

@[protected]

theorem isometry_equiv.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

source

@[protected]

theorem isometry_equiv.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

source

@[protected]

theorem isometry_equiv.continuous {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

continuous ⇑h

source

@[simp]

theorem isometry_equiv.ediam_image {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) (s : set α) :

emetric.diam (⇑h '' s) = emetric.diam s

source

theorem isometry_equiv.to_equiv_inj {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] ⦃h₁ h₂ : α ≃ᵢ β⦄ :

h₁.to_equiv = h₂.to_equiv → h₁ = h₂

source

@[ext]

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

h₁ = h₂

source

def isometry_equiv.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

isometry_equiv.mk' f g hfg hf = {to_equiv := {to_fun := f, inv_fun := g, left_inv := _, right_inv := hfg}, isometry_to_fun := hf}

source

@[protected]

def isometry_equiv.refl (α : Type u_1) [pseudo_emetric_space α] :

α ≃ᵢ α

The identity isometry of a space.

Equations

isometry_equiv.refl α = {to_equiv := {to_fun := (equiv.refl α).to_fun, inv_fun := (equiv.refl α).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}

source

@[protected]

def isometry_equiv.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.

Equations

h₁.trans h₂ = {to_equiv := {to_fun := (h₁.to_equiv.trans h₂.to_equiv).to_fun, inv_fun := (h₁.to_equiv.trans h₂.to_equiv).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}

source

@[simp]

theorem isometry_equiv.trans_apply {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : α) :

⇑(h₁.trans h₂) x = ⇑h₂ (⇑h₁ x)

source

@[protected]

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

β ≃ᵢ α

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

Equations

h.symm = {to_equiv := h.to_equiv.symm, isometry_to_fun := _}

source

def isometry_equiv.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

isometry_equiv.simps.apply h = ⇑h

source

def isometry_equiv.simps.symm_apply {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

β → α

See Note [custom simps projection]

Equations

isometry_equiv.simps.symm_apply h = ⇑(h.symm)

source

@[simp]

theorem isometry_equiv.symm_symm {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

h.symm.symm = h

source

@[simp]

theorem isometry_equiv.apply_symm_apply {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) (y : β) :

⇑h (⇑(h.symm) y) = y

source

@[simp]

theorem isometry_equiv.symm_apply_apply {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) (x : α) :

⇑(h.symm) (⇑h x) = x

source

theorem isometry_equiv.symm_apply_eq {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) {x : α} {y : β} :

⇑(h.symm) y = x ↔ y = ⇑h x

source

theorem isometry_equiv.eq_symm_apply {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) {x : α} {y : β} :

x = ⇑(h.symm) y ↔ ⇑h x = y

source

theorem isometry_equiv.symm_comp_self {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

⇑(h.symm) ∘ ⇑h = id

source

theorem isometry_equiv.self_comp_symm {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

⇑h ∘ ⇑(h.symm) = id

source

@[simp]

theorem isometry_equiv.range_eq_univ {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

set.range ⇑h = set.univ

source

theorem isometry_equiv.image_symm {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

set.image ⇑(h.symm) = set.preimage ⇑h

source

theorem isometry_equiv.preimage_symm {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

set.preimage ⇑(h.symm) = set.image ⇑h

source

@[simp]

theorem isometry_equiv.symm_trans_apply {α : Type u} {β : Type v} {γ : Type w} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : γ) :

⇑((h₁.trans h₂).symm) x = ⇑(h₁.symm) (⇑(h₂.symm) x)

source

theorem isometry_equiv.ediam_univ {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

emetric.diam set.univ = emetric.diam set.univ

source

@[simp]

theorem isometry_equiv.ediam_preimage {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) (s : set β) :

emetric.diam (⇑h ⁻¹' s) = emetric.diam s

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[protected]

def isometry_equiv.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 := _}

source

@[simp]

theorem isometry_equiv.to_homeomorph_to_equiv {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

h.to_homeomorph.to_equiv = h.to_equiv

source

@[simp]

theorem isometry_equiv.coe_to_homeomorph {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

⇑(h.to_homeomorph) = ⇑h

source

@[simp]

theorem isometry_equiv.coe_to_homeomorph_symm {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (h : α ≃ᵢ β) :

⇑(h.to_homeomorph.symm) = ⇑(h.symm)

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[protected, instance]

def isometry_equiv.group {α : Type u} [pseudo_emetric_space α] :

group (α ≃ᵢ α)

The group of isometries.

Equations

isometry_equiv.group = {mul := λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁, mul_assoc := _, one := isometry_equiv.refl α _inst_1, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (isometry_equiv.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometry_equiv.group._proof_4 isometry_equiv.group._proof_5, npow_zero' := _, npow_succ' := _, inv := isometry_equiv.symm _inst_1, div := div_inv_monoid.div._default (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometry_equiv.group._proof_8 (isometry_equiv.refl α) isometry_equiv.group._proof_9 isometry_equiv.group._proof_10 (div_inv_monoid.npow._default (isometry_equiv.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometry_equiv.group._proof_4 isometry_equiv.group._proof_5) isometry_equiv.group._proof_11 isometry_equiv.group._proof_12 isometry_equiv.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometry_equiv.group._proof_14 (isometry_equiv.refl α) isometry_equiv.group._proof_15 isometry_equiv.group._proof_16 (div_inv_monoid.npow._default (isometry_equiv.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometry_equiv.group._proof_4 isometry_equiv.group._proof_5) isometry_equiv.group._proof_17 isometry_equiv.group._proof_18 isometry_equiv.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

source

@[simp]

theorem isometry_equiv.coe_one {α : Type u} [pseudo_emetric_space α] :

⇑1 = id

source

@[simp]

theorem isometry_equiv.coe_mul {α : Type u} [pseudo_emetric_space α] (e₁ e₂ : α ≃ᵢ α) :

⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

source

theorem isometry_equiv.mul_apply {α : Type u} [pseudo_emetric_space α] (e₁ e₂ : α ≃ᵢ α) (x : α) :

⇑(e₁ * e₂) x = ⇑e₁ (⇑e₂ x)

source

@[simp]

theorem isometry_equiv.inv_apply_self {α : Type u} [pseudo_emetric_space α] (e : α ≃ᵢ α) (x : α) :

⇑e⁻¹ (⇑e x) = x

source

@[simp]

theorem isometry_equiv.apply_inv_self {α : Type u} [pseudo_emetric_space α] (e : α ≃ᵢ α) (x : α) :

⇑e (⇑e⁻¹ x) = x

source

@[protected]

theorem isometry_equiv.complete_space {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] [complete_space β] (e : α ≃ᵢ β) :

complete_space α

source

theorem isometry_equiv.complete_space_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (e : α ≃ᵢ β) :

complete_space α ↔ complete_space β

source

def isometry_equiv.fun_unique (ι : Type u_1) (α : Type u) [pseudo_emetric_space α] [unique ι] [fintype ι] :

(ι → α) ≃ᵢ α

equiv.fun_unique as an isometry_equiv.

Equations

isometry_equiv.fun_unique ι α = {to_equiv := equiv.fun_unique ι α _inst_4, isometry_to_fun := _}

source

@[simp]

theorem isometry_equiv.fun_unique_apply (ι : Type u_1) (α : Type u) [pseudo_emetric_space α] [unique ι] [fintype ι] (f : Π (x : ι), (λ (a' : ι), (λ (ᾰ : ι), α) a') x) :

⇑(isometry_equiv.fun_unique ι α) f = f inhabited.default

source

@[simp]

theorem isometry_equiv.fun_unique_symm_apply (ι : Type u_1) (α : Type u) [pseudo_emetric_space α] [unique ι] [fintype ι] (x : α) (b : ι) :

⇑((isometry_equiv.fun_unique ι α).symm) x b = x

source

@[simp]

theorem isometry_equiv.fun_unique_to_equiv (ι : Type u_1) (α : Type u) [pseudo_emetric_space α] [unique ι] [fintype ι] :

(isometry_equiv.fun_unique ι α).to_equiv = equiv.fun_unique ι α

source

@[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) :

⇑(isometry_equiv.pi_fin_two α) f = (f 0, f 1)

source

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

isometry_equiv.pi_fin_two α = {to_equiv := pi_fin_two_equiv α, isometry_to_fun := _}

source

@[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)) :

⇑((isometry_equiv.pi_fin_two α).symm) p i = fin.cons p.fst (fin.cons p.snd fin_zero_elim) i

source

@[simp]

theorem isometry_equiv.pi_fin_two_to_equiv (α : fin 2 → Type u_1) [Π (i : fin 2), pseudo_emetric_space (α i)] :

(isometry_equiv.pi_fin_two α).to_equiv = pi_fin_two_equiv α

source

@[simp]

theorem isometry_equiv.diam_image {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] (h : α ≃ᵢ β) (s : set α) :

metric.diam (⇑h '' s) = metric.diam s

source

@[simp]

theorem isometry_equiv.diam_preimage {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] (h : α ≃ᵢ β) (s : set β) :

metric.diam (⇑h ⁻¹' s) = metric.diam s

source

theorem isometry_equiv.diam_univ {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] (h : α ≃ᵢ β) :

metric.diam set.univ = metric.diam set.univ

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry_equiv.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

source

@[simp]

theorem isometry.isometry_equiv_on_range_to_equiv {α : Type u} {β : Type v} [emetric_space α] [pseudo_emetric_space β] {f : α → β} (h : isometry f) :

h.isometry_equiv_on_range.to_equiv = equiv.of_injective f _

source

noncomputable def isometry.isometry_equiv_on_range {α : Type u} {β : Type v} [emetric_space α] [pseudo_emetric_space β] {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.isometry_equiv_on_range = {to_equiv := equiv.of_injective f _, isometry_to_fun := _}

source

@[simp]

theorem isometry.isometry_equiv_on_range_apply {α : Type u} {β : Type v} [emetric_space α] [pseudo_emetric_space β] {f : α → β} (h : isometry f) (a : α) :

⇑(h.isometry_equiv_on_range) a = ⟨f a, _⟩

mathlib3 documentation

Isometries #