mathlib3 documentation

analysis.normed_space.affine_isometry

Affine isometries #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 seminormed_add_comm_group and specialize to normed_add_comm_group 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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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.

Instances for affine_isometry
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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]
@[protected, 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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (f : P →ᵃⁱ[𝕜] 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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (p1 p2 : P) :
(f.linear_isometry) (p1 -ᵥ p2) = f p1 -ᵥ f p2
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P) :
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P) :
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P) :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :
@[protected]
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 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [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 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [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 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂] (f₁ : P₁ →ᵃⁱ[𝕜] P₂) {x y : P₁} (h : x y) :
f₁ x f₁ y
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :
@[protected, continuity]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] :
P →ᵃⁱ[𝕜] P

The identity affine isometry.

Equations
@[simp]
theorem affine_isometry.id_apply {𝕜 : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] (x : P) :
@[protected, instance]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃] [pseudo_metric_space P] [pseudo_metric_space P₂] [pseudo_metric_space P₃] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃] [pseudo_metric_space P] [pseudo_metric_space P₂] [pseudo_metric_space P₃] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] [normed_add_torsor V₃ P₃] (g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) :
(g.comp f) = g f
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] [seminormed_add_comm_group V₄] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃] [normed_space 𝕜 V₄] [pseudo_metric_space P] [pseudo_metric_space P₂] [pseudo_metric_space P₃] [pseudo_metric_space P₄] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] [normed_add_torsor V₃ P₃] [normed_add_torsor V₄ P₄] (f : P₃ →ᵃⁱ[𝕜] P₄) (g : P₂ →ᵃⁱ[𝕜] P₃) (h : P →ᵃⁱ[𝕜] P₂) :
(f.comp g).comp h = f.comp (g.comp h)
@[protected, instance]
def affine_isometry.monoid {𝕜 : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] :
@[simp]
theorem affine_isometry.coe_mul {𝕜 : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] (f g : P →ᵃⁱ[𝕜] P) :
(f * g) = f g
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] :
Type (max u_2 u_4 u_8 u_9)

A affine isometric equivalence between two normed vector spaces.

Instances for affine_isometry_equiv
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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
@[protected, 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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] 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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] {e e' : P ≃ᵃⁱ[𝕜] P₂} (h : (x : P), e x = e' x) :
e = e'
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [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 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [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 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂) :
V ≃ᵃⁱ[𝕜] V₂

Reinterpret a linear isometry equiv as an affine isometry equiv.

Equations
@[simp]
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
def affine_isometry_equiv.to_isometry_equiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_4} {P : Type u_8} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
P ≃ᵢ P₂

Reinterpret a affine_isometry_equiv as an isometry_equiv.

Equations
@[simp]
theorem affine_isometry_equiv.coe_to_isometry_equiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_4} {P : Type u_8} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x : P} :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {s : set P} :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {s : set P} {x : P} :
@[protected, instance]
Equations
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[simp]
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃] [pseudo_metric_space P] [pseudo_metric_space P₂] [pseudo_metric_space P₃] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃] [pseudo_metric_space P] [pseudo_metric_space P₂] [pseudo_metric_space P₃] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[simp]
theorem affine_isometry_equiv.self_trans_symm {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_4} {P : Type u_8} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[simp]
theorem affine_isometry_equiv.symm_trans_self {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_4} {P : Type u_8} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] 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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃] [pseudo_metric_space P] [pseudo_metric_space P₂] [pseudo_metric_space P₃] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] [seminormed_add_comm_group V₄] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃] [normed_space 𝕜 V₄] [pseudo_metric_space P] [pseudo_metric_space P₂] [pseudo_metric_space P₃] [pseudo_metric_space P₄] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] [normed_add_torsor V₃ P₃] [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'
@[protected, instance]

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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] (e e' : P ≃ᵃⁱ[𝕜] P) :
(e * e') = e e'
@[simp]
theorem affine_isometry_equiv.coe_inv {𝕜 : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x y : P) :
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x y : P) :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x y : P} (h : x y) :
e x e y
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [normed_add_torsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected]
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] (p : P) :
V ≃ᵃⁱ[𝕜] 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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] (p : P) :
((affine_isometry_equiv.vadd_const 𝕜 p).symm) = λ (p' : P), p' -ᵥ p
def affine_isometry_equiv.const_vsub (𝕜 : Type u_1) {V : Type u_2} {P : Type u_8} [normed_field 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] (p : P) :
P ≃ᵃⁱ[𝕜] V

p' ↦ p -ᵥ p' as an affine isometric equivalence.

Equations
def affine_isometry_equiv.const_vadd (𝕜 : Type u_1) {V : Type u_2} (P : Type u_8) [normed_field 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] (v : V) :
P ≃ᵃⁱ[𝕜] P

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

Equations
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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.

Point reflection in x as an affine isometric automorphism.

Equations
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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P] [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.

@[simp]
theorem affine_subspace.equiv_map_of_injective_apply {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_4} {P₁ : Type u_7} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂] (E : affine_subspace 𝕜 P₁) [nonempty E] (φ : P₁ →ᵃ[𝕜] P₂) (hφ : function.injective φ) (ᾰ : E) :
@[simp]
noncomputable def affine_subspace.equiv_map_of_injective {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_4} {P₁ : Type u_7} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂] (E : affine_subspace 𝕜 P₁) [nonempty E] (φ : P₁ →ᵃ[𝕜] P₂) (hφ : function.injective φ) :

An affine subspace is isomorphic to its image under an injective affine map. This is the affine version of submodule.equiv_map_of_injective.

Equations
@[simp]
theorem affine_subspace.equiv_map_of_injective_symm_apply {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_4} {P₁ : Type u_7} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂] (E : affine_subspace 𝕜 P₁) [nonempty E] (φ : P₁ →ᵃ[𝕜] P₂) (hφ : function.injective φ) (ᾰ : (φ '' E)) :
noncomputable def affine_subspace.isometry_equiv_map {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_4} {P₁ : Type u_7} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂] (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] :

Restricts an affine isometry to an affine isometry equivalence between a nonempty affine subspace E and its image.

This is an isometry version of affine_subspace.equiv_map, having a stronger premise and a stronger conclusion.

Equations
@[simp]
theorem affine_subspace.isometry_equiv_map.apply_symm_apply {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_4} {P₁ : Type u_7} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂] {E : affine_subspace 𝕜 P₁} [nonempty E] {φ : P₁ →ᵃⁱ[𝕜] P₂} (x : (affine_subspace.map φ.to_affine_map E)) :
@[simp]
theorem affine_subspace.isometry_equiv_map.coe_apply {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_4} {P₁ : Type u_7} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂] (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] (g : E) :
@[simp]
theorem affine_subspace.isometry_equiv_map.to_affine_map_eq {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_4} {P₁ : Type u_7} {P₂ : Type u_9} [normed_field 𝕜] [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [metric_space P₁] [pseudo_metric_space P₂] [normed_add_torsor V₁ P₁] [normed_add_torsor V₂ P₂] (φ : P₁ →ᵃⁱ[𝕜] P₂) (E : affine_subspace 𝕜 P₁) [nonempty E] :