mathlib documentation

analysis.normed_space.affine_isometry

Affine isometries #

In this file we define affine_isometry π•œ P Pβ‚‚ to be an affine isometric embedding of normed add-torsors P into Pβ‚‚ over normed π•œ-spaces and affine_isometry_equiv to be an affine isometric equivalence between P and Pβ‚‚.

We also prove basic lemmas and provide convenience constructors. The choice of these lemmas and constructors is closely modelled on those for the linear_isometry and affine_map theories.

Since many elementary properties don't require βˆ₯xβˆ₯ = 0 β†’ x = 0 we initially set up the theory for semi_normed_add_torsor and specialize to normed_add_torsor only when needed.

Notation #

We introduce the notation P →ᡃⁱ[π•œ] Pβ‚‚ for affine_isometry π•œ P Pβ‚‚, and P ≃ᡃⁱ[π•œ] Pβ‚‚ for affine_isometry_equiv π•œ P Pβ‚‚. In contrast with the notation β†’β‚—α΅’ for linear isometries, ≃ᡒ for isometric equivalences, etc., the "i" here is a superscript. This is for aesthetic reasons to match the superscript "a" (note that in mathlib →ᡃ is an affine map, since →ₐ has been taken by algebra-homomorphisms.)

structure affine_isometry (π•œ : Type u_1) {V : Type u_2} {Vβ‚‚ : Type u_4} (P : Type u_8) (Pβ‚‚ : Type u_9) [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] :
Type (max u_2 u_4 u_8 u_9)

An π•œ-affine isometric embedding of one normed add-torsor over a normed π•œ-space into another.

def affine_isometry.linear_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
V β†’β‚—α΅’[π•œ] Vβ‚‚

The underlying linear map of an affine isometry is in fact a linear isometry.

Equations
@[simp]
theorem affine_isometry.linear_eq_linear_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
@[instance]
def affine_isometry.has_coe_to_fun {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] :
has_coe_to_fun (P →ᡃⁱ[π•œ] Pβ‚‚) (Ξ» (_x : P →ᡃⁱ[π•œ] Pβ‚‚), P β†’ Pβ‚‚)
Equations
@[simp]
theorem affine_isometry.coe_to_affine_map {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry.to_affine_map_injective {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] :
theorem affine_isometry.coe_fn_injective {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] :
@[ext]
theorem affine_isometry.ext {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] {f g : P →ᡃⁱ[π•œ] Pβ‚‚} (h : βˆ€ (x : P), ⇑f x = ⇑g x) :
f = g
def linear_isometry.to_affine_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (f : V β†’β‚—α΅’[π•œ] Vβ‚‚) :
V →ᡃⁱ[π•œ] Vβ‚‚

Reinterpret a linear isometry as an affine isometry.

Equations
@[simp]
theorem linear_isometry.coe_to_affine_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (f : V β†’β‚—α΅’[π•œ] Vβ‚‚) :
@[simp]
theorem linear_isometry.to_affine_isometry_linear_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (f : V β†’β‚—α΅’[π•œ] Vβ‚‚) :
@[simp]
theorem linear_isometry.to_affine_isometry_to_affine_map {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (f : V β†’β‚—α΅’[π•œ] Vβ‚‚) :
@[simp]
theorem affine_isometry.map_vadd {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) (p : P) (v : V) :
@[simp]
theorem affine_isometry.map_vsub {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) (p1 p2 : P) :
@[simp]
theorem affine_isometry.dist_map {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) (x y : P) :
dist (⇑f x) (⇑f y) = dist x y
@[simp]
theorem affine_isometry.nndist_map {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) (x y : P) :
nndist (⇑f x) (⇑f y) = nndist x y
@[simp]
theorem affine_isometry.edist_map {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) (x y : P) :
edist (⇑f x) (⇑f y) = edist x y
theorem affine_isometry.isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry.injective {π•œ : Type u_1} {V₁ : Type u_3} {Vβ‚‚ : Type u_4} {P₁ : Type u_7} {Pβ‚‚ : Type u_9} [normed_field π•œ] [normed_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f₁ : P₁ →ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry.map_eq_iff {π•œ : Type u_1} {V₁ : Type u_3} {Vβ‚‚ : Type u_4} {P₁ : Type u_7} {Pβ‚‚ : Type u_9} [normed_field π•œ] [normed_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f₁ : P₁ →ᡃⁱ[π•œ] Pβ‚‚) {x y : P₁} :
⇑f₁ x = ⇑f₁ y ↔ x = y
theorem affine_isometry.map_ne {π•œ : Type u_1} {V₁ : Type u_3} {Vβ‚‚ : Type u_4} {P₁ : Type u_7} {Pβ‚‚ : Type u_9} [normed_field π•œ] [normed_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f₁ : P₁ →ᡃⁱ[π•œ] Pβ‚‚) {x y : P₁} (h : x β‰  y) :
⇑f₁ x β‰  ⇑f₁ y
theorem affine_isometry.lipschitz {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry.antilipschitz {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry.continuous {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry.ediam_image {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) (s : set P) :
theorem affine_isometry.ediam_range {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry.diam_image {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) (s : set P) :
theorem affine_isometry.diam_range {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry.comp_continuous_iff {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) {Ξ± : Type u_3} [topological_space Ξ±] {g : Ξ± β†’ P} :
def affine_isometry.id {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :

The identity affine isometry.

Equations
@[simp]
theorem affine_isometry.coe_id {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
@[simp]
theorem affine_isometry.id_apply {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (x : P) :
@[simp]
theorem affine_isometry.id_to_affine_map {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
@[instance]
def affine_isometry.inhabited {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
Equations
def affine_isometry.comp {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {V₃ : Type u_5} {P : Type u_8} {Pβ‚‚ : Type u_9} {P₃ : Type u_10} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_group V₃] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [semi_normed_space π•œ V₃] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [pseudo_metric_space P₃] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [semi_normed_add_torsor V₃ P₃] (g : Pβ‚‚ →ᡃⁱ[π•œ] P₃) (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
P →ᡃⁱ[π•œ] P₃

Composition of affine isometries.

Equations
@[simp]
theorem affine_isometry.coe_comp {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {V₃ : Type u_5} {P : Type u_8} {Pβ‚‚ : Type u_9} {P₃ : Type u_10} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_group V₃] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [semi_normed_space π•œ V₃] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [pseudo_metric_space P₃] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [semi_normed_add_torsor V₃ P₃] (g : Pβ‚‚ →ᡃⁱ[π•œ] P₃) (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry.id_comp {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry.comp_id {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (f : P →ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry.comp_assoc {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {V₃ : Type u_5} {Vβ‚„ : Type u_6} {P : Type u_8} {Pβ‚‚ : Type u_9} {P₃ : Type u_10} {Pβ‚„ : Type u_11} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_group V₃] [semi_normed_group Vβ‚„] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [semi_normed_space π•œ V₃] [semi_normed_space π•œ Vβ‚„] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [pseudo_metric_space P₃] [pseudo_metric_space Pβ‚„] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [semi_normed_add_torsor V₃ P₃] [semi_normed_add_torsor Vβ‚„ Pβ‚„] (f : P₃ →ᡃⁱ[π•œ] Pβ‚„) (g : Pβ‚‚ →ᡃⁱ[π•œ] P₃) (h : P →ᡃⁱ[π•œ] Pβ‚‚) :
(f.comp g).comp h = f.comp (g.comp h)
@[instance]
def affine_isometry.monoid {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
Equations
@[simp]
theorem affine_isometry.coe_one {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
@[simp]
theorem affine_isometry.coe_mul {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (f g : P →ᡃⁱ[π•œ] P) :
structure affine_isometry_equiv (π•œ : Type u_1) {V : Type u_2} {Vβ‚‚ : Type u_4} (P : Type u_8) (Pβ‚‚ : Type u_9) [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] :
Type (max u_2 u_4 u_8 u_9)

A affine isometric equivalence between two normed vector spaces.

def affine_isometry_equiv.linear_isometry_equiv {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
V ≃ₗᡒ[π•œ] Vβ‚‚

The underlying linear equiv of an affine isometry equiv is in fact a linear isometry equiv.

Equations
@[simp]
theorem affine_isometry_equiv.linear_eq_linear_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
@[instance]
def affine_isometry_equiv.has_coe_to_fun {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] :
has_coe_to_fun (P ≃ᡃⁱ[π•œ] Pβ‚‚) (Ξ» (_x : P ≃ᡃⁱ[π•œ] Pβ‚‚), P β†’ Pβ‚‚)
Equations
@[simp]
theorem affine_isometry_equiv.coe_mk {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃ[π•œ] Pβ‚‚) (he : βˆ€ (x : V), βˆ₯⇑(e.linear) xβˆ₯ = βˆ₯xβˆ₯) :
@[simp]
theorem affine_isometry_equiv.coe_to_affine_equiv {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry_equiv.to_affine_equiv_injective {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] :
@[ext]
theorem affine_isometry_equiv.ext {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] {e e' : P ≃ᡃⁱ[π•œ] Pβ‚‚} (h : βˆ€ (x : P), ⇑e x = ⇑e' x) :
e = e'
def affine_isometry_equiv.to_affine_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
P →ᡃⁱ[π•œ] Pβ‚‚

Reinterpret a affine_isometry_equiv as a affine_isometry.

Equations
@[simp]
theorem affine_isometry_equiv.coe_to_affine_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
def affine_isometry_equiv.mk' {π•œ : Type u_1} {V₁ : Type u_3} {Vβ‚‚ : Type u_4} {P₁ : Type u_7} {Pβ‚‚ : Type u_9} [normed_field π•œ] [normed_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P₁ β†’ Pβ‚‚) (e' : V₁ ≃ₗᡒ[π•œ] Vβ‚‚) (p : P₁) (h : βˆ€ (p' : P₁), e p' = ⇑e' (p' -α΅₯ p) +α΅₯ e p) :
P₁ ≃ᡃⁱ[π•œ] Pβ‚‚

Construct an affine isometry equivalence by verifying the relation between the map and its linear part at one base point. Namely, this function takes a map e : P₁ β†’ Pβ‚‚, a linear isometry equivalence e' : V₁ ≃ᡒₗ[k] Vβ‚‚, and a point p such that for any other point p' we have e p' = e' (p' -α΅₯ p) +α΅₯ e p.

Equations
@[simp]
theorem affine_isometry_equiv.coe_mk' {π•œ : Type u_1} {V₁ : Type u_3} {Vβ‚‚ : Type u_4} {P₁ : Type u_7} {Pβ‚‚ : Type u_9} [normed_field π•œ] [normed_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P₁ β†’ Pβ‚‚) (e' : V₁ ≃ₗᡒ[π•œ] Vβ‚‚) (p : P₁) (h : βˆ€ (p' : P₁), e p' = ⇑e' (p' -α΅₯ p) +α΅₯ e p) :
@[simp]
theorem affine_isometry_equiv.linear_isometry_equiv_mk' {π•œ : Type u_1} {V₁ : Type u_3} {Vβ‚‚ : Type u_4} {P₁ : Type u_7} {Pβ‚‚ : Type u_9} [normed_field π•œ] [normed_group V₁] [semi_normed_group Vβ‚‚] [normed_space π•œ V₁] [semi_normed_space π•œ Vβ‚‚] [metric_space P₁] [pseudo_metric_space Pβ‚‚] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P₁ β†’ Pβ‚‚) (e' : V₁ ≃ₗᡒ[π•œ] Vβ‚‚) (p : P₁) (h : βˆ€ (p' : P₁), e p' = ⇑e' (p' -α΅₯ p) +α΅₯ e p) :
def linear_isometry_equiv.to_affine_isometry_equiv {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (e : V ≃ₗᡒ[π•œ] Vβ‚‚) :
V ≃ᡃⁱ[π•œ] Vβ‚‚

Reinterpret a linear isometry equiv as an affine isometry equiv.

Equations
@[simp]
theorem linear_isometry_equiv.coe_to_affine_isometry_equiv {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (e : V ≃ₗᡒ[π•œ] Vβ‚‚) :
@[simp]
theorem linear_isometry_equiv.to_affine_isometry_equiv_linear_isometry_equiv {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (e : V ≃ₗᡒ[π•œ] Vβ‚‚) :
@[simp]
theorem linear_isometry_equiv.to_affine_isometry_equiv_to_affine_equiv {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (e : V ≃ₗᡒ[π•œ] Vβ‚‚) :
@[simp]
theorem linear_isometry_equiv.to_affine_isometry_equiv_to_affine_isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] (e : V ≃ₗᡒ[π•œ] Vβ‚‚) :
theorem affine_isometry_equiv.isometry {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
def affine_isometry_equiv.to_isometric {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
P ≃ᡒ Pβ‚‚

Reinterpret a affine_isometry_equiv as an isometric.

Equations
@[simp]
theorem affine_isometry_equiv.coe_to_isometric {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry_equiv.range_eq_univ {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
def affine_isometry_equiv.to_homeomorph {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
P β‰ƒβ‚œ Pβ‚‚

Reinterpret a affine_isometry_equiv as an homeomorph.

Equations
@[simp]
theorem affine_isometry_equiv.coe_to_homeomorph {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry_equiv.continuous {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry_equiv.continuous_at {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) {x : P} :
theorem affine_isometry_equiv.continuous_on {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) {s : set P} :
theorem affine_isometry_equiv.continuous_within_at {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) {s : set P} {x : P} :
def affine_isometry_equiv.refl (π•œ : Type u_1) {V : Type u_2} (P : Type u_8) [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :

Identity map as a affine_isometry_equiv.

Equations
@[instance]
def affine_isometry_equiv.inhabited {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
Equations
@[simp]
theorem affine_isometry_equiv.coe_refl {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
@[simp]
theorem affine_isometry_equiv.to_affine_equiv_refl {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
@[simp]
theorem affine_isometry_equiv.to_isometric_refl {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
@[simp]
theorem affine_isometry_equiv.to_homeomorph_refl {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
def affine_isometry_equiv.symm {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
Pβ‚‚ ≃ᡃⁱ[π•œ] P

The inverse affine_isometry_equiv.

Equations
@[simp]
theorem affine_isometry_equiv.apply_symm_apply {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (x : Pβ‚‚) :
⇑e (⇑(e.symm) x) = x
@[simp]
theorem affine_isometry_equiv.symm_apply_apply {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (x : P) :
⇑(e.symm) (⇑e x) = x
@[simp]
theorem affine_isometry_equiv.symm_symm {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
e.symm.symm = e
@[simp]
theorem affine_isometry_equiv.to_affine_equiv_symm {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry_equiv.to_isometric_symm {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry_equiv.to_homeomorph_symm {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
def affine_isometry_equiv.trans {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {V₃ : Type u_5} {P : Type u_8} {Pβ‚‚ : Type u_9} {P₃ : Type u_10} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_group V₃] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [semi_normed_space π•œ V₃] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [pseudo_metric_space P₃] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [semi_normed_add_torsor V₃ P₃] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (e' : Pβ‚‚ ≃ᡃⁱ[π•œ] P₃) :
P ≃ᡃⁱ[π•œ] P₃

Composition of affine_isometry_equivs as a affine_isometry_equiv.

Equations
@[simp]
theorem affine_isometry_equiv.coe_trans {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {V₃ : Type u_5} {P : Type u_8} {Pβ‚‚ : Type u_9} {P₃ : Type u_10} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_group V₃] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [semi_normed_space π•œ V₃] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [pseudo_metric_space P₃] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [semi_normed_add_torsor V₃ P₃] (e₁ : P ≃ᡃⁱ[π•œ] Pβ‚‚) (eβ‚‚ : Pβ‚‚ ≃ᡃⁱ[π•œ] P₃) :
⇑(e₁.trans eβ‚‚) = ⇑eβ‚‚ ∘ ⇑e₁
@[simp]
theorem affine_isometry_equiv.trans_refl {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
e.trans (affine_isometry_equiv.refl π•œ Pβ‚‚) = e
@[simp]
theorem affine_isometry_equiv.refl_trans {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry_equiv.trans_symm {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry_equiv.symm_trans {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
e.symm.trans e = affine_isometry_equiv.refl π•œ Pβ‚‚
@[simp]
theorem affine_isometry_equiv.coe_symm_trans {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {V₃ : Type u_5} {P : Type u_8} {Pβ‚‚ : Type u_9} {P₃ : Type u_10} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_group V₃] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [semi_normed_space π•œ V₃] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [pseudo_metric_space P₃] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [semi_normed_add_torsor V₃ P₃] (e₁ : P ≃ᡃⁱ[π•œ] Pβ‚‚) (eβ‚‚ : Pβ‚‚ ≃ᡃⁱ[π•œ] P₃) :
⇑((e₁.trans eβ‚‚).symm) = ⇑(e₁.symm) ∘ ⇑(eβ‚‚.symm)
theorem affine_isometry_equiv.trans_assoc {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {V₃ : Type u_5} {Vβ‚„ : Type u_6} {P : Type u_8} {Pβ‚‚ : Type u_9} {P₃ : Type u_10} {Pβ‚„ : Type u_11} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_group V₃] [semi_normed_group Vβ‚„] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [semi_normed_space π•œ V₃] [semi_normed_space π•œ Vβ‚„] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [pseudo_metric_space P₃] [pseudo_metric_space Pβ‚„] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] [semi_normed_add_torsor V₃ P₃] [semi_normed_add_torsor Vβ‚„ Pβ‚„] (ePPβ‚‚ : P ≃ᡃⁱ[π•œ] Pβ‚‚) (ePβ‚‚G : Pβ‚‚ ≃ᡃⁱ[π•œ] P₃) (eGG' : P₃ ≃ᡃⁱ[π•œ] Pβ‚„) :
ePPβ‚‚.trans (ePβ‚‚G.trans eGG') = (ePPβ‚‚.trans ePβ‚‚G).trans eGG'
@[instance]
def affine_isometry_equiv.group {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :

The group of affine isometries of a normed_add_torsor, P.

Equations
@[simp]
theorem affine_isometry_equiv.coe_one {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
@[simp]
theorem affine_isometry_equiv.coe_mul {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (e e' : P ≃ᡃⁱ[π•œ] P) :
@[simp]
theorem affine_isometry_equiv.coe_inv {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (e : P ≃ᡃⁱ[π•œ] P) :
@[simp]
theorem affine_isometry_equiv.map_vadd {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (p : P) (v : V) :
@[simp]
theorem affine_isometry_equiv.map_vsub {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (p1 p2 : P) :
@[simp]
theorem affine_isometry_equiv.dist_map {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (x y : P) :
dist (⇑e x) (⇑e y) = dist x y
@[simp]
theorem affine_isometry_equiv.edist_map {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (x y : P) :
edist (⇑e x) (⇑e y) = edist x y
theorem affine_isometry_equiv.bijective {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry_equiv.injective {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry_equiv.surjective {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry_equiv.map_eq_iff {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) {x y : P} :
⇑e x = ⇑e y ↔ x = y
theorem affine_isometry_equiv.map_ne {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) {x y : P} (h : x β‰  y) :
theorem affine_isometry_equiv.lipschitz {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
theorem affine_isometry_equiv.antilipschitz {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) :
@[simp]
theorem affine_isometry_equiv.ediam_image {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (s : set P) :
@[simp]
theorem affine_isometry_equiv.diam_image {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) (s : set P) :
@[simp]
theorem affine_isometry_equiv.comp_continuous_on_iff {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) {Ξ± : Type u_12} [topological_space Ξ±] {f : Ξ± β†’ P} {s : set Ξ±} :
@[simp]
theorem affine_isometry_equiv.comp_continuous_iff {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] (e : P ≃ᡃⁱ[π•œ] Pβ‚‚) {Ξ± : Type u_12} [topological_space Ξ±] {f : Ξ± β†’ P} :
def affine_isometry_equiv.vadd_const (π•œ : Type u_1) {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (p : P) :

The map v ↦ v +α΅₯ p as an affine isometric equivalence between V and P.

Equations
@[simp]
theorem affine_isometry_equiv.coe_vadd_const {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (p : P) :
⇑(affine_isometry_equiv.vadd_const π•œ p) = Ξ» (v : V), v +α΅₯ p
@[simp]
theorem affine_isometry_equiv.coe_vadd_const_symm {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (p : P) :
⇑((affine_isometry_equiv.vadd_const π•œ p).symm) = Ξ» (p' : P), p' -α΅₯ p
@[simp]
theorem affine_isometry_equiv.vadd_const_to_affine_equiv {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (p : P) :
def affine_isometry_equiv.const_vsub (π•œ : Type u_1) {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (p : P) :

p' ↦ p -α΅₯ p' as an affine isometric equivalence.

Equations
@[simp]
theorem affine_isometry_equiv.coe_const_vsub {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (p : P) :
@[simp]
def affine_isometry_equiv.const_vadd (π•œ : Type u_1) {V : Type u_2} (P : Type u_8) [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (v : V) :

Translation by v (that is, the map p ↦ v +α΅₯ p) as an affine isometric automorphism of P.

Equations
@[simp]
theorem affine_isometry_equiv.coe_const_vadd {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (v : V) :
@[simp]
theorem affine_isometry_equiv.const_vadd_zero {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] :
theorem affine_isometry_equiv.vadd_vsub {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] {f : P β†’ Pβ‚‚} (hf : isometry f) {p : P} {g : V β†’ Vβ‚‚} (hg : βˆ€ (v : V), g v = f (v +α΅₯ p) -α΅₯ f p) :

The map g from V to Vβ‚‚ corresponding to a map f from P to Pβ‚‚, at a base point p, is an isometry if f is one.

def affine_isometry_equiv.point_reflection (π•œ : Type u_1) {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (x : P) :

Point reflection in x as an affine isometric automorphism.

Equations
theorem affine_isometry_equiv.point_reflection_apply {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (x y : P) :
@[simp]
theorem affine_isometry_equiv.point_reflection_self {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (x : P) :
@[simp]
theorem affine_isometry_equiv.point_reflection_symm {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (x : P) :
@[simp]
theorem affine_isometry_equiv.dist_point_reflection_fixed {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (x y : P) :
theorem affine_isometry_equiv.dist_point_reflection_self' {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (x y : P) :
theorem affine_isometry_equiv.dist_point_reflection_self {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] (x y : P) :
theorem affine_isometry_equiv.point_reflection_fixed_iff {π•œ : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π•œ] [semi_normed_group V] [semi_normed_space π•œ V] [pseudo_metric_space P] [semi_normed_add_torsor V P] [invertible 2] {x y : P} :
theorem affine_map.continuous_linear_iff {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] {f : P →ᡃ[π•œ] Pβ‚‚} :

If f is an affine map, then its linear part is continuous iff f is continuous.

theorem affine_map.is_open_map_linear_iff {π•œ : Type u_1} {V : Type u_2} {Vβ‚‚ : Type u_4} {P : Type u_8} {Pβ‚‚ : Type u_9} [normed_field π•œ] [semi_normed_group V] [semi_normed_group Vβ‚‚] [semi_normed_space π•œ V] [semi_normed_space π•œ Vβ‚‚] [pseudo_metric_space P] [pseudo_metric_space Pβ‚‚] [semi_normed_add_torsor V P] [semi_normed_add_torsor Vβ‚‚ Pβ‚‚] {f : P →ᡃ[π•œ] Pβ‚‚} :

If f is an affine map, then its linear part is an open map iff f is an open map.