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

source
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
source
@[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
source
@[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β‚‚) :
f.to_affine_map.linear = f.linear_isometry.to_linear_map
source
@[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
source
@[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β‚‚) :
⇑(f.to_affine_map) = ⇑f
source
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β‚‚] :
function.injective affine_isometry.to_affine_map
source
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β‚‚] :
function.injective coe_fn
source
@[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
source
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
source
@[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β‚‚) :
⇑(f.to_affine_isometry) = ⇑f
source
@[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β‚‚) :
f.to_affine_isometry.linear_isometry = f
source
@[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β‚‚) :
f.to_affine_isometry.to_affine_map = f.to_linear_map.to_affine_map
source
@[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) :
⇑f (v +α΅₯ p) = ⇑(f.linear_isometry) v +α΅₯ ⇑f p
source
@[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
source
@[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) :
has_dist.dist (⇑f x) (⇑f y) = has_dist.dist x y
source
@[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) :
has_nndist.nndist (⇑f x) (⇑f y) = has_nndist.nndist x y
source
@[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) :
has_edist.edist (⇑f x) (⇑f y) = has_edist.edist x y
source
@[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β‚‚) :
isometry ⇑f
source
@[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β‚‚) :
function.injective ⇑f₁
source
@[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
source
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
source
@[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β‚‚) :
lipschitz_with 1 ⇑f
source
@[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β‚‚) :
antilipschitz_with 1 ⇑f
source
@[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β‚‚) :
continuous ⇑f
source
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) :
emetric.diam (⇑f '' s) = emetric.diam s
source
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β‚‚) :
emetric.diam (set.range ⇑f) = emetric.diam set.univ
source
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) :
metric.diam (⇑f '' s) = metric.diam s
source
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β‚‚) :
metric.diam (set.range ⇑f) = metric.diam set.univ
source
@[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} :
continuous (⇑f ∘ g) ↔ continuous g
source
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
source
@[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] :
⇑affine_isometry.id = id
source
@[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) :
⇑affine_isometry.id x = x
source
@[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] :
affine_isometry.id.to_affine_map = affine_map.id π•œ P
source
@[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] :
inhabited (P →ᡃⁱ[π•œ] P)
Equations
source
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
source
@[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
source
@[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β‚‚) :
affine_isometry.id.comp f = f
source
@[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β‚‚) :
f.comp affine_isometry.id = f
source
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)
source
@[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] :
monoid (P →ᡃⁱ[π•œ] P)
Equations
source
@[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] :
⇑1 = id
source
@[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
source
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
source
@[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
source
@[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β‚‚) :
e.to_affine_equiv.linear = e.linear_isometry_equiv.to_linear_equiv
source
@[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
source
@[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βˆ₯) :
⇑{to_affine_equiv := e, norm_map := he} = ⇑e
source
@[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β‚‚) :
⇑(e.to_affine_equiv) = ⇑e
source
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β‚‚] :
function.injective affine_isometry_equiv.to_affine_equiv
source
@[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'
source
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
source
@[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β‚‚) :
⇑(e.to_affine_isometry) = ⇑e
source
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
source
@[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) :
⇑(affine_isometry_equiv.mk' e e' p h) = e
source
@[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) :
(affine_isometry_equiv.mk' e e' p h).linear_isometry_equiv = e'
source
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
source
@[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β‚‚) :
⇑(e.to_affine_isometry_equiv) = ⇑e
source
@[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β‚‚) :
e.to_affine_isometry_equiv.linear_isometry_equiv = e
source
@[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β‚‚) :
e.to_affine_isometry_equiv.to_affine_equiv = e.to_linear_equiv.to_affine_equiv
source
@[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β‚‚) :
e.to_affine_isometry_equiv.to_affine_isometry = e.to_linear_isometry.to_affine_isometry
source
@[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β‚‚) :
isometry ⇑e
source
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
source
@[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β‚‚) :
⇑(e.to_isometric) = ⇑e
source
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β‚‚) :
set.range ⇑e = set.univ
source
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
source
@[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β‚‚) :
⇑(e.to_homeomorph) = ⇑e
source
@[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β‚‚) :
continuous ⇑e
source
@[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} :
continuous_at ⇑e x
source
@[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} :
continuous_on ⇑e s
source
@[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} :
continuous_within_at ⇑e s x
source
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] :
P ≃ᡃⁱ[π•œ] P

Identity map as a affine_isometry_equiv.

Equations
source
@[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] :
inhabited (P ≃ᡃⁱ[π•œ] P)
Equations
source
@[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] :
⇑(affine_isometry_equiv.refl π•œ P) = id
source
@[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] :
(affine_isometry_equiv.refl π•œ P).to_affine_equiv = affine_equiv.refl π•œ P
source
@[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] :
(affine_isometry_equiv.refl π•œ P).to_isometric = isometric.refl P
source
@[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] :
(affine_isometry_equiv.refl π•œ P).to_homeomorph = homeomorph.refl P
source
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
source
@[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
source
@[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
source
@[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
source
@[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β‚‚) :
e.to_affine_equiv.symm = e.symm.to_affine_equiv
source
@[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β‚‚) :
e.to_isometric.symm = e.symm.to_isometric
source
@[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β‚‚) :
e.to_homeomorph.symm = e.symm.to_homeomorph
source
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
source
@[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₁
source
@[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
source
@[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β‚‚) :
(affine_isometry_equiv.refl π•œ P).trans e = e
source
@[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β‚‚) :
e.trans e.symm = affine_isometry_equiv.refl π•œ P
source
@[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β‚‚
source
@[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)
source
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'
source
@[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] :
group (P ≃ᡃⁱ[π•œ] P)

The group of affine isometries of a normed_add_torsor, P.

Equations
source
@[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] :
⇑1 = id
source
@[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'
source
@[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) :
⇑e⁻¹ = ⇑(e.symm)
source
@[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) :
⇑e (v +α΅₯ p) = ⇑(e.linear_isometry_equiv) v +α΅₯ ⇑e p
source
@[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) :
⇑(e.linear_isometry_equiv) (p1 -α΅₯ p2) = ⇑e p1 -α΅₯ ⇑e p2
source
@[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) :
has_dist.dist (⇑e x) (⇑e y) = has_dist.dist x y
source
@[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) :
has_edist.edist (⇑e x) (⇑e y) = has_edist.edist x y
source
@[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β‚‚) :
function.bijective ⇑e
source
@[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β‚‚) :
function.injective ⇑e
source
@[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β‚‚) :
function.surjective ⇑e
source
@[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
source
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
source
@[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β‚‚) :
lipschitz_with 1 ⇑e
source
@[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β‚‚) :
antilipschitz_with 1 ⇑e
source
@[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) :
emetric.diam (⇑e '' s) = emetric.diam s
source
@[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) :
metric.diam (⇑e '' s) = metric.diam s
source
@[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 Ξ±} :
continuous_on (⇑e ∘ f) s ↔ continuous_on f s
source
@[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} :
continuous (⇑e ∘ f) ↔ continuous f
source
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
source
@[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
source
@[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
source
@[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) :
(affine_isometry_equiv.vadd_const π•œ p).to_affine_equiv = affine_equiv.vadd_const π•œ p
source
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
source
@[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) :
⇑(affine_isometry_equiv.const_vsub π•œ p) = has_vsub.vsub p
source
@[simp]
theorem affine_isometry_equiv.symm_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) :
(affine_isometry_equiv.const_vsub π•œ p).symm = (linear_isometry_equiv.neg π•œ).to_affine_isometry_equiv.trans (affine_isometry_equiv.vadd_const π•œ p)
source
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
source
@[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) :
⇑(affine_isometry_equiv.const_vadd π•œ P v) = has_vadd.vadd v
source
@[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] :
affine_isometry_equiv.const_vadd π•œ P 0 = affine_isometry_equiv.refl π•œ P
source
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) :
isometry g

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.

source
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) :
P ≃ᡃⁱ[π•œ] P

Point reflection in x as an affine isometric automorphism.

Equations
source
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) :
⇑(affine_isometry_equiv.point_reflection π•œ x) y = x -α΅₯ y +α΅₯ x
source
@[simp]
theorem affine_isometry_equiv.point_reflection_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] (x : P) :
(affine_isometry_equiv.point_reflection π•œ x).to_affine_equiv = affine_equiv.point_reflection π•œ x
source
@[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) :
⇑(affine_isometry_equiv.point_reflection π•œ x) x = x
source
theorem affine_isometry_equiv.point_reflection_involutive {π•œ : 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) :
function.involutive ⇑(affine_isometry_equiv.point_reflection π•œ x)
source
@[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) :
(affine_isometry_equiv.point_reflection π•œ x).symm = affine_isometry_equiv.point_reflection π•œ x
source
@[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) :
has_dist.dist (⇑(affine_isometry_equiv.point_reflection π•œ x) y) x = has_dist.dist y x
source
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) :
has_dist.dist (⇑(affine_isometry_equiv.point_reflection π•œ x) y) y = βˆ₯bit0 (x -α΅₯ y)βˆ₯
source
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) :
has_dist.dist (⇑(affine_isometry_equiv.point_reflection π•œ x) y) y = βˆ₯2βˆ₯ * has_dist.dist x y
source
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} :
⇑(affine_isometry_equiv.point_reflection π•œ x) y = y ↔ y = x
source
theorem affine_isometry_equiv.dist_point_reflection_self_real {V : Type u_2} {P : Type u_8} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] [normed_space ℝ V] (x y : P) :
has_dist.dist (⇑(affine_isometry_equiv.point_reflection ℝ x) y) y = 2 * has_dist.dist x y
source
@[simp]
theorem affine_isometry_equiv.point_reflection_midpoint_left {V : Type u_2} {P : Type u_8} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] [normed_space ℝ V] (x y : P) :
⇑(affine_isometry_equiv.point_reflection ℝ (midpoint ℝ x y)) x = y
source
@[simp]
theorem affine_isometry_equiv.point_reflection_midpoint_right {V : Type u_2} {P : Type u_8} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] [normed_space ℝ V] (x y : P) :
⇑(affine_isometry_equiv.point_reflection ℝ (midpoint ℝ x y)) y = x
source
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β‚‚} :
continuous ⇑(f.linear) ↔ continuous ⇑f

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

source
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β‚‚} :
is_open_map ⇑(f.linear) ↔ is_open_map ⇑f

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