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 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]
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 𝕜] [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, 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₂) :
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 𝕜] [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₂] :
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 𝕜] [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₂] :
@[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 linear_isometry.to_affine_isometry_linear_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 linear_isometry.to_affine_isometry_to_affine_map {𝕜 : 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) :
@[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] :

The identity affine isometry.

Equations
@[simp]
theorem affine_isometry.coe_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] :
@[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) :
@[simp]
theorem affine_isometry.id_to_affine_map {𝕜 : 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] :
@[protected, instance]
def affine_isometry.inhabited {𝕜 : 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
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₂) :
@[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) :
@[simp]
theorem affine_subspace.coe_subtypeₐᵢ {𝕜 : 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] (s : affine_subspace 𝕜 P) [nonempty ↥s] :
@[simp]
theorem affine_subspace.subtypeₐᵢ_to_affine_map {𝕜 : 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] (s : affine_subspace 𝕜 P) [nonempty ↥s] :
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
@[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 𝕜] [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, 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₂) :
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 𝕜] [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₂] :
@[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'
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 𝕜] [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 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 𝕜] [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]
theorem linear_isometry_equiv.coe_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₂) :
@[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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [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 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V] [normed_space 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂) :
@[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_isometric {𝕜 : 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 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 𝕜] [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} :
def affine_isometry_equiv.refl (𝕜 : 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] :

Identity map as a affine_isometry_equiv.

Equations
@[protected, instance]
def affine_isometry_equiv.inhabited {𝕜 : 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_equiv.coe_refl {𝕜 : 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.to_affine_equiv_refl {𝕜 : 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.to_isometric_refl {𝕜 : 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.to_homeomorph_refl {𝕜 : 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] :
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]
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 𝕜] [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.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₂) :
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 𝕜] [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₂) :
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 𝕜] [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]
def affine_isometry_equiv.group {𝕜 : 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] :

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

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
@[simp]
theorem affine_isometry_equiv.vadd_const_to_affine_equiv {𝕜 : 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) :
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' ↦ 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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [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 𝕜] [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.

def affine_isometry_equiv.point_reflection (𝕜 : 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) :

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 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V] [pseudo_metric_space P] [normed_add_torsor V P] (x y : P) :
@[simp]
@[simp]
theorem affine_isometry_equiv.point_reflection_self {𝕜 : 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) :
@[simp]
theorem affine_isometry_equiv.point_reflection_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] (x : P) :
@[simp]
theorem affine_isometry_equiv.dist_point_reflection_fixed {𝕜 : 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 y : P) :
theorem affine_isometry_equiv.dist_point_reflection_self' {𝕜 : 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 y : P) :
theorem affine_isometry_equiv.dist_point_reflection_self {𝕜 : 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 y : P) :
theorem affine_isometry_equiv.point_reflection_fixed_iff {𝕜 : 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] [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 𝕜] [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.