# mathlibdocumentation

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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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.

@[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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [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 π] [semi_normed_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 π] [semi_normed_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 π] [semi_normed_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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (f : P βα΅β±[π] Pβ) (x y : P) :
nndist (βf x) (βf y) = 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (f : P βα΅β±[π] Pβ) (x y : P) :
edist (βf x) (βf y) = y
@[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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [normed_group Vβ] [semi_normed_group Vβ] [normed_space π Vβ] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ 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β] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ 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β] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (f : P βα΅β±[π] Pβ) {Ξ± : Type u_3} {g : Ξ± β P} :
def affine_isometry.id {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :

The identity affine isometry.

Equations
@[simp]
theorem affine_isometry.coe_id {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
@[simp]
theorem affine_isometry.id_apply {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (x : P) :
@[simp]
theorem affine_isometry.id_to_affine_map {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
@[protected, instance]
def affine_isometry.inhabited {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
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β] [normed_space π V] [normed_space π Vβ] [normed_space π Vβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [normed_space π Vβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ Pβ] (g : Pβ βα΅β±[π] Pβ) (f : P βα΅β±[π] Pβ) :
β(g.comp 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [normed_space π Vβ] [normed_space π Vβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ Pβ] [ 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 π] [normed_space π V]  :
Equations
@[simp]
theorem affine_isometry.coe_one {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
@[simp]
theorem affine_isometry.coe_mul {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (f g : P βα΅β±[π] P) :
β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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] :
Type (max u_2 u_4 u_8 u_9)

A affine isometric equivalence between two normed vector spaces.

@[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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ 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β] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ Pβ] (e : Pβ β Pβ) (e' : Vβ ββα΅’[π] Vβ) (p : Pβ) (h : β (p' : Pβ), e p' = βe' (p' -α΅₯ p) +α΅₯ e p) :
β p h) = e
@[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β] [normed_space π Vβ] [metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ 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β] [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 π] [semi_normed_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 π] [semi_normed_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 π] [semi_normed_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 π] [semi_normed_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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [normed_space π V]  :

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 π] [normed_space π V]  :
Equations
@[simp]
theorem affine_isometry_equiv.coe_refl {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
@[simp]
theorem affine_isometry_equiv.to_affine_equiv_refl {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
= P
@[simp]
theorem affine_isometry_equiv.to_isometric_refl {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
@[simp]
theorem affine_isometry_equiv.to_homeomorph_refl {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [normed_space π Vβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ Pβ] (e : P βα΅β±[π] Pβ) (e' : Pβ βα΅β±[π] Pβ) :
P βα΅β±[π] Pβ

Composition of `affine_isometry_equiv`s 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β] [normed_space π V] [normed_space π Vβ] [normed_space π Vβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (e : P βα΅β±[π] Pβ) :
e.trans 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (e : P βα΅β±[π] Pβ) :
P).trans e = e
@[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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (e : P βα΅β±[π] Pβ) :
e.trans e.symm =
@[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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (e : P βα΅β±[π] Pβ) :
e.symm.trans e = 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β] [normed_space π V] [normed_space π Vβ] [normed_space π Vβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [normed_space π Vβ] [normed_space π Vβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [pseudo_metric_space Pβ] [ Pβ] [ Pβ] [ 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 π] [normed_space π V]  :

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 π] [normed_space π V]  :
@[simp]
theorem affine_isometry_equiv.coe_mul {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (e e' : P βα΅β±[π] P) :
@[simp]
theorem affine_isometry_equiv.coe_inv {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (e : P βα΅β±[π] Pβ) (x y : P) :
edist (βe x) (βe y) = y
@[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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [semi_normed_group Vβ] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (e : P βα΅β±[π] Pβ) {Ξ± : Type u_12} {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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] (e : P βα΅β±[π] Pβ) {Ξ± : Type u_12} {f : Ξ± β P} :
def affine_isometry_equiv.vadd_const (π : Type u_1) {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (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 π] [normed_space π V] (p : P) :
β 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 π] [normed_space π V] (p : P) :
β 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 π] [normed_space π V] (p : P) :
def affine_isometry_equiv.const_vsub (π : Type u_1) {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (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 π] [normed_space π V] (p : P) :
@[simp]
theorem affine_isometry_equiv.symm_const_vsub {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (p : P) :
def affine_isometry_equiv.const_vadd (π : Type u_1) {V : Type u_2} (P : Type u_8) [normed_field π] [normed_space π V] (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 π] [normed_space π V] (v : V) :
β v) =
@[simp]
theorem affine_isometry_equiv.const_vadd_zero {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V]  :
0 =
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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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 π] [normed_space π V] (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 π] [normed_space π V] (x y : P) :
@[simp]
theorem affine_isometry_equiv.point_reflection_to_affine_equiv {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (x : P) :
@[simp]
theorem affine_isometry_equiv.point_reflection_self {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (x : P) :
= x
theorem affine_isometry_equiv.point_reflection_involutive {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (x : P) :
@[simp]
theorem affine_isometry_equiv.point_reflection_symm {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (x : P) :
@[simp]
theorem affine_isometry_equiv.dist_point_reflection_fixed {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (x y : P) :
dist y) x = dist y x
theorem affine_isometry_equiv.dist_point_reflection_self' {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (x y : P) :
theorem affine_isometry_equiv.dist_point_reflection_self {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] (x y : P) :
theorem affine_isometry_equiv.point_reflection_fixed_iff {π : Type u_1} {V : Type u_2} {P : Type u_8} [normed_field π] [normed_space π V] [invertible 2] {x y : P} :
= y β y = x
theorem affine_isometry_equiv.dist_point_reflection_self_real {V : Type u_2} {P : Type u_8} [ V] (x y : P) :
= 2 * dist x y
@[simp]
theorem affine_isometry_equiv.point_reflection_midpoint_left {V : Type u_2} {P : Type u_8} [ V] (x y : P) :
= y
@[simp]
theorem affine_isometry_equiv.point_reflection_midpoint_right {V : Type u_2} {P : Type u_8} [ V] (x y : P) :
= x
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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ 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β] [normed_space π V] [normed_space π Vβ] [pseudo_metric_space Pβ] [ Pβ] {f : P βα΅[π] Pβ} :

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