Documentation

Mathlib.Analysis.Normed.Affine.Isometry

Affine isometries #

In this file we define AffineIsometry 𝕜 P P₂ to be an affine isometric embedding of normed add-torsors P into P₂ over normed 𝕜-spaces and AffineIsometryEquiv 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 LinearIsometry and AffineMap theories.

Since many elementary properties don't require ‖x‖ = 0 → x = 0 we initially set up the theory for SeminormedAddCommGroup and specialize to NormedAddCommGroup only when needed.

Notation #

We introduce the notation P →ᵃⁱ[𝕜] P₂ for AffineIsometry 𝕜 P P₂, and P ≃ᵃⁱ[𝕜] P₂ for AffineIsometryEquiv 𝕜 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 AffineIsometry (𝕜 : Type u_1) {V : Type u_2} {V₂ : Type u_5} (P : Type u_10) (P₂ : Type u_11) [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] extends P →ᵃ[𝕜] P₂ :

Type (max (max (max u_10 u_11) u_2) u_5)

A 𝕜-affine isometric embedding of one normed add-torsor over a normed 𝕜-space into another, denoted as f : P →ᵃⁱ[𝕜] P₂.

toFun : P → P₂
linear : V →ₗ[𝕜] V₂
map_vadd' (p : P) (v : V) : self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun p
norm_map (x : V) : ‖self.linear x‖ = ‖x‖

Instances For

def «term_→ᵃⁱ[_]_» :

Lean.TrailingParserDescr

A 𝕜-affine isometric embedding of one normed add-torsor over a normed 𝕜-space into another, denoted as f : P →ᵃⁱ[𝕜] P₂.

Equations

One or more equations did not get rendered due to their size.

def AffineIsometry.linearIsometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

V →ₗᵢ[𝕜] V₂

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

Equations

f.linearIsometry = { toLinearMap := f.linear, norm_map' := ⋯ }

@[simp]

theorem AffineIsometry.linear_eq_linearIsometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

f.linear = f.linearIsometry.toLinearMap

instance AffineIsometry.instFunLike {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] :

FunLike (P →ᵃⁱ[𝕜] P₂) P P₂

Equations

AffineIsometry.instFunLike = { coe := fun (f : P →ᵃⁱ[𝕜] P₂) => f.toFun, coe_injective' := ⋯ }

@[simp]

theorem AffineIsometry.coe_toAffineMap {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

⇑f.toAffineMap = ⇑f

theorem AffineIsometry.toAffineMap_injective {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] :

Function.Injective toAffineMap

theorem AffineIsometry.coeFn_injective {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] :

Function.Injective DFunLike.coe

theorem AffineIsometry.ext {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] {f g : P →ᵃⁱ[𝕜] P₂} (h : ∀ (x : P), f x = g x) :

f = g

def LinearIsometry.toAffineIsometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (f : V →ₗᵢ[𝕜] V₂) :

V →ᵃⁱ[𝕜] V₂

Reinterpret a linear isometry as an affine isometry.

Equations

f.toAffineIsometry = { toAffineMap := f.toAffineMap, norm_map := ⋯ }

@[simp]

theorem LinearIsometry.coe_toAffineIsometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (f : V →ₗᵢ[𝕜] V₂) :

⇑f.toAffineIsometry = ⇑f

@[simp]

theorem LinearIsometry.toAffineIsometry_linearIsometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (f : V →ₗᵢ[𝕜] V₂) :

f.toAffineIsometry.linearIsometry = f

@[simp]

theorem LinearIsometry.toAffineIsometry_toAffineMap {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (f : V →ₗᵢ[𝕜] V₂) :

f.toAffineIsometry.toAffineMap = f.toAffineMap

@[simp]

theorem AffineIsometry.map_vadd {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (p : P) (v : V) :

f (v +ᵥ p) = f.linearIsometry v +ᵥ f p

@[simp]

theorem AffineIsometry.map_vsub {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (p1 p2 : P) :

f.linearIsometry (p1 -ᵥ p2) = f p1 -ᵥ f p2

@[simp]

theorem AffineIsometry.dist_map {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P) :

dist (f x) (f y) = dist x y

@[simp]

theorem AffineIsometry.nndist_map {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P) :

nndist (f x) (f y) = nndist x y

@[simp]

theorem AffineIsometry.edist_map {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (x y : P) :

edist (f x) (f y) = edist x y

theorem AffineIsometry.isometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

theorem AffineIsometry.injective {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁'] [NormedSpace 𝕜 V₁'] [MetricSpace P₁'] [NormedAddTorsor V₁' P₁'] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f₁ : P₁' →ᵃⁱ[𝕜] P₂) :

Function.Injective ⇑f₁

@[simp]

theorem AffineIsometry.map_eq_iff {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁'] [NormedSpace 𝕜 V₁'] [MetricSpace P₁'] [NormedAddTorsor V₁' P₁'] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f₁ : P₁' →ᵃⁱ[𝕜] P₂) {x y : P₁'} :

f₁ x = f₁ y ↔ x = y

theorem AffineIsometry.map_ne {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁'] [NormedSpace 𝕜 V₁'] [MetricSpace P₁'] [NormedAddTorsor V₁' P₁'] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f₁ : P₁' →ᵃⁱ[𝕜] P₂) {x y : P₁'} (h : x ≠ y) :

f₁ x ≠ f₁ y

theorem AffineIsometry.lipschitz {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

LipschitzWith 1 ⇑f

theorem AffineIsometry.antilipschitz {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

AntilipschitzWith 1 ⇑f

theorem AffineIsometry.continuous {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

Continuous ⇑f

theorem AffineIsometry.ediam_image {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (s : Set P) :

EMetric.diam (⇑f '' s) = EMetric.diam s

theorem AffineIsometry.ediam_range {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

EMetric.diam (Set.range ⇑f) = EMetric.diam Set.univ

theorem AffineIsometry.diam_image {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) (s : Set P) :

Metric.diam (⇑f '' s) = Metric.diam s

theorem AffineIsometry.diam_range {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

Metric.diam (Set.range ⇑f) = Metric.diam Set.univ

@[simp]

theorem AffineIsometry.comp_continuous_iff {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) {α : Type u_14} [TopologicalSpace α] {g : α → P} :

Continuous (⇑f ∘ g) ↔ Continuous g

def AffineIsometry.id {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

P →ᵃⁱ[𝕜] P

The identity affine isometry.

Equations

AffineIsometry.id = { toAffineMap := AffineMap.id 𝕜 P, norm_map := ⋯ }

@[simp]

theorem AffineIsometry.coe_id {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

⇑id = _root_.id

@[simp]

theorem AffineIsometry.id_apply {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :

id x = x

@[simp]

theorem AffineIsometry.id_toAffineMap {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

id.toAffineMap = AffineMap.id 𝕜 P

instance AffineIsometry.instInhabited {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

Inhabited (P →ᵃⁱ[𝕜] P)

Equations

AffineIsometry.instInhabited = { default := AffineIsometry.id }

def AffineIsometry.comp {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] [SeminormedAddCommGroup V₃] [NormedSpace 𝕜 V₃] [PseudoMetricSpace P₃] [NormedAddTorsor V₃ P₃] (g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) :

P →ᵃⁱ[𝕜] P₃

Composition of affine isometries.

Equations

g.comp f = { toAffineMap := g.comp f.toAffineMap, norm_map := ⋯ }

@[simp]

theorem AffineIsometry.coe_comp {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] [SeminormedAddCommGroup V₃] [NormedSpace 𝕜 V₃] [PseudoMetricSpace P₃] [NormedAddTorsor V₃ P₃] (g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) :

⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem AffineIsometry.id_comp {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

@[simp]

theorem AffineIsometry.comp_id {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂) :

theorem AffineIsometry.comp_assoc {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {V₄ : Type u_7} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12} {P₄ : Type u_13} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] [SeminormedAddCommGroup V₃] [NormedSpace 𝕜 V₃] [PseudoMetricSpace P₃] [NormedAddTorsor V₃ P₃] [SeminormedAddCommGroup V₄] [NormedSpace 𝕜 V₄] [PseudoMetricSpace P₄] [NormedAddTorsor V₄ P₄] (f : P₃ →ᵃⁱ[𝕜] P₄) (g : P₂ →ᵃⁱ[𝕜] P₃) (h : P →ᵃⁱ[𝕜] P₂) :

(f.comp g).comp h = f.comp (g.comp h)

instance AffineIsometry.instMonoid {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

Monoid (P →ᵃⁱ[𝕜] P)

Equations

AffineIsometry.instMonoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

@[simp]

theorem AffineIsometry.coe_one {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

⇑1 = _root_.id

@[simp]

theorem AffineIsometry.coe_mul {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (f g : P →ᵃⁱ[𝕜] P) :

⇑(f * g) = ⇑f ∘ ⇑g

def AffineSubspace.subtypeₐᵢ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] :

↥s →ᵃⁱ[𝕜] P

AffineSubspace.subtype as an AffineIsometry.

Equations

s.subtypeₐᵢ = { toAffineMap := s.subtype, norm_map := ⋯ }

theorem AffineSubspace.subtypeₐᵢ_linear {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] :

s.subtypeₐᵢ.linear = s.direction.subtype

@[simp]

theorem AffineSubspace.subtypeₐᵢ_linearIsometry {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] :

s.subtypeₐᵢ.linearIsometry = s.direction.subtypeₗᵢ

@[simp]

theorem AffineSubspace.coe_subtypeₐᵢ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] :

⇑s.subtypeₐᵢ = ⇑s.subtype

@[simp]

theorem AffineSubspace.subtypeₐᵢ_toAffineMap {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace 𝕜 P) [Nonempty ↥s] :

s.subtypeₐᵢ.toAffineMap = s.subtype

structure AffineIsometryEquiv (𝕜 : Type u_1) {V : Type u_2} {V₂ : Type u_5} (P : Type u_10) (P₂ : Type u_11) [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] extends P ≃ᵃ[𝕜] P₂ :

Type (max (max (max u_10 u_11) u_2) u_5)

An affine isometric equivalence between two normed vector spaces, denoted f : P ≃ᵃⁱ[𝕜] P₂.

toFun : P → P₂
invFun : P₂ → P
left_inv : Function.LeftInverse self.invFun self.toFun
right_inv : Function.RightInverse self.invFun self.toFun
linear : V ≃ₗ[𝕜] V₂
map_vadd' (p : P) (v : V) : self.toEquiv (v +ᵥ p) = self.linear v +ᵥ self.toEquiv p
norm_map (x : V) : ‖self.linear x‖ = ‖x‖

Instances For

def «term_≃ᵃⁱ[_]_» :

Lean.TrailingParserDescr

An affine isometric equivalence between two normed vector spaces, denoted f : P ≃ᵃⁱ[𝕜] P₂.

Equations

One or more equations did not get rendered due to their size.

def AffineIsometryEquiv.linearIsometryEquiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

V ≃ₗᵢ[𝕜] V₂

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

Equations

e.linearIsometryEquiv = { toLinearEquiv := e.linear, norm_map' := ⋯ }

@[simp]

theorem AffineIsometryEquiv.linear_eq_linear_isometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

e.linear = e.linearIsometryEquiv.toLinearEquiv

instance AffineIsometryEquiv.instEquivLike {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] :

EquivLike (P ≃ᵃⁱ[𝕜] P₂) P P₂

Equations

AffineIsometryEquiv.instEquivLike = { coe := fun (f : P ≃ᵃⁱ[𝕜] P₂) => f.toFun, inv := fun (f : P ≃ᵃⁱ[𝕜] P₂) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_mk {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃ[𝕜] P₂) (he : ∀ (x : V), ‖e.linear x‖ = ‖x‖) :

⇑{ toAffineEquiv := e, norm_map := he } = ⇑e

@[simp]

theorem AffineIsometryEquiv.coe_toAffineEquiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

⇑e.toAffineEquiv = ⇑e

theorem AffineIsometryEquiv.toAffineEquiv_injective {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] :

Function.Injective toAffineEquiv

theorem AffineIsometryEquiv.ext {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] {e e' : P ≃ᵃⁱ[𝕜] P₂} (h : ∀ (x : P), e x = e' x) :

e = e'

def AffineIsometryEquiv.toAffineIsometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

P →ᵃⁱ[𝕜] P₂

Reinterpret an AffineIsometryEquiv as an AffineIsometry.

Equations

e.toAffineIsometry = { toAffineMap := ↑e.toAffineEquiv, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_toAffineIsometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

⇑e.toAffineIsometry = ⇑e

def AffineIsometryEquiv.mk' {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁] [NormedSpace 𝕜 V₁] [PseudoMetricSpace P₁] [NormedAddTorsor V₁ P₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor 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

AffineIsometryEquiv.mk' e e' p h = { toAffineEquiv := AffineEquiv.mk' e e'.toLinearEquiv p h, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_mk' {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁] [NormedSpace 𝕜 V₁] [PseudoMetricSpace P₁] [NormedAddTorsor V₁ P₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :

⇑(mk' e e' p h) = e

@[simp]

theorem AffineIsometryEquiv.linearIsometryEquiv_mk' {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁] [NormedSpace 𝕜 V₁] [PseudoMetricSpace P₁] [NormedAddTorsor V₁ P₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) :

(mk' e e' p h).linearIsometryEquiv = e'

def LinearIsometryEquiv.toAffineIsometryEquiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂) :

V ≃ᵃⁱ[𝕜] V₂

Reinterpret a linear isometry equiv as an affine isometry equiv.

Equations

e.toAffineIsometryEquiv = { toAffineEquiv := e.toAffineEquiv, norm_map := ⋯ }

@[simp]

theorem LinearIsometryEquiv.coe_toAffineIsometryEquiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂) :

⇑e.toAffineIsometryEquiv = ⇑e

@[simp]

theorem LinearIsometryEquiv.toAffineIsometryEquiv_linearIsometryEquiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂) :

e.toAffineIsometryEquiv.linearIsometryEquiv = e

@[simp]

theorem LinearIsometryEquiv.toAffineIsometryEquiv_toAffineEquiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂) :

e.toAffineIsometryEquiv.toAffineEquiv = e.toAffineEquiv

@[simp]

theorem LinearIsometryEquiv.toAffineIsometryEquiv_toAffineIsometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂) :

e.toAffineIsometryEquiv.toAffineIsometry = e.toLinearIsometry.toAffineIsometry

theorem AffineIsometryEquiv.isometry {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

def AffineIsometryEquiv.toIsometryEquiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

P ≃ᵢ P₂

Reinterpret an AffineIsometryEquiv as an IsometryEquiv.

Equations

e.toIsometryEquiv = { toEquiv := e.toEquiv, isometry_toFun := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_toIsometryEquiv {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

⇑e.toIsometryEquiv = ⇑e

theorem AffineIsometryEquiv.range_eq_univ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

Set.range ⇑e = Set.univ

def AffineIsometryEquiv.toHomeomorph {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

P ≃ₜ P₂

Reinterpret an AffineIsometryEquiv as a Homeomorph.

Equations

e.toHomeomorph = e.toIsometryEquiv.toHomeomorph

@[simp]

theorem AffineIsometryEquiv.coe_toHomeomorph {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

⇑e.toHomeomorph = ⇑e

theorem AffineIsometryEquiv.continuous {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

Continuous ⇑e

theorem AffineIsometryEquiv.continuousAt {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x : P} :

ContinuousAt (⇑e) x

theorem AffineIsometryEquiv.continuousOn {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {s : Set P} :

ContinuousOn (⇑e) s

theorem AffineIsometryEquiv.continuousWithinAt {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {s : Set P} {x : P} :

ContinuousWithinAt (⇑e) s x

def AffineIsometryEquiv.refl (𝕜 : Type u_1) {V : Type u_2} (P : Type u_10) [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

P ≃ᵃⁱ[𝕜] P

Identity map as an AffineIsometryEquiv.

Equations

AffineIsometryEquiv.refl 𝕜 P = { toAffineEquiv := AffineEquiv.refl 𝕜 P, norm_map := ⋯ }

instance AffineIsometryEquiv.instInhabited {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

Inhabited (P ≃ᵃⁱ[𝕜] P)

Equations

AffineIsometryEquiv.instInhabited = { default := AffineIsometryEquiv.refl 𝕜 P }

@[simp]

theorem AffineIsometryEquiv.coe_refl {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

⇑(refl 𝕜 P) = id

@[simp]

theorem AffineIsometryEquiv.toAffineEquiv_refl {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

(refl 𝕜 P).toAffineEquiv = AffineEquiv.refl 𝕜 P

@[simp]

theorem AffineIsometryEquiv.toIsometryEquiv_refl {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

(refl 𝕜 P).toIsometryEquiv = IsometryEquiv.refl P

@[simp]

theorem AffineIsometryEquiv.toHomeomorph_refl {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

(refl 𝕜 P).toHomeomorph = Homeomorph.refl P

def AffineIsometryEquiv.symm {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

P₂ ≃ᵃⁱ[𝕜] P

The inverse AffineIsometryEquiv.

Equations

e.symm = { toAffineEquiv := e.symm, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.apply_symm_apply {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x : P₂) :

e (e.symm x) = x

@[simp]

theorem AffineIsometryEquiv.symm_apply_apply {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x : P) :

e.symm (e x) = x

@[simp]

theorem AffineIsometryEquiv.symm_symm {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

e.symm.symm = e

theorem AffineIsometryEquiv.symm_bijective {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] :

Function.Bijective symm

@[simp]

theorem AffineIsometryEquiv.toAffineEquiv_symm {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

e.symm = e.symm.toAffineEquiv

@[simp]

theorem AffineIsometryEquiv.toIsometryEquiv_symm {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

e.toIsometryEquiv.symm = e.symm.toIsometryEquiv

@[simp]

theorem AffineIsometryEquiv.toHomeomorph_symm {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

e.toHomeomorph.symm = e.symm.toHomeomorph

def AffineIsometryEquiv.trans {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] [SeminormedAddCommGroup V₃] [NormedSpace 𝕜 V₃] [PseudoMetricSpace P₃] [NormedAddTorsor V₃ P₃] (e : P ≃ᵃⁱ[𝕜] P₂) (e' : P₂ ≃ᵃⁱ[𝕜] P₃) :

P ≃ᵃⁱ[𝕜] P₃

Composition of AffineIsometryEquivs as an AffineIsometryEquiv.

Equations

e.trans e' = { toAffineEquiv := e.trans e'.toAffineEquiv, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_trans {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] [SeminormedAddCommGroup V₃] [NormedSpace 𝕜 V₃] [PseudoMetricSpace P₃] [NormedAddTorsor V₃ P₃] (e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) :

⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

@[simp]

theorem AffineIsometryEquiv.trans_refl {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

e.trans (refl 𝕜 P₂) = e

@[simp]

theorem AffineIsometryEquiv.refl_trans {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

(refl 𝕜 P).trans e = e

@[simp]

theorem AffineIsometryEquiv.self_trans_symm {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

e.trans e.symm = refl 𝕜 P

@[simp]

theorem AffineIsometryEquiv.symm_trans_self {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

e.symm.trans e = refl 𝕜 P₂

@[simp]

theorem AffineIsometryEquiv.coe_symm_trans {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] [SeminormedAddCommGroup V₃] [NormedSpace 𝕜 V₃] [PseudoMetricSpace P₃] [NormedAddTorsor V₃ P₃] (e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) :

⇑(e₁.trans e₂).symm = ⇑e₁.symm ∘ ⇑e₂.symm

theorem AffineIsometryEquiv.trans_assoc {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {V₄ : Type u_7} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12} {P₄ : Type u_13} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] [SeminormedAddCommGroup V₃] [NormedSpace 𝕜 V₃] [PseudoMetricSpace P₃] [NormedAddTorsor V₃ P₃] [SeminormedAddCommGroup V₄] [NormedSpace 𝕜 V₄] [PseudoMetricSpace P₄] [NormedAddTorsor V₄ P₄] (ePP₂ : P ≃ᵃⁱ[𝕜] P₂) (eP₂G : P₂ ≃ᵃⁱ[𝕜] P₃) (eGG' : P₃ ≃ᵃⁱ[𝕜] P₄) :

ePP₂.trans (eP₂G.trans eGG') = (ePP₂.trans eP₂G).trans eGG'

instance AffineIsometryEquiv.instGroup {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

Group (P ≃ᵃⁱ[𝕜] P)

The group of affine isometries of a NormedAddTorsor, P.

Equations

AffineIsometryEquiv.instGroup = Group.mk ⋯

@[simp]

theorem AffineIsometryEquiv.coe_one {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

⇑1 = id

@[simp]

theorem AffineIsometryEquiv.coe_mul {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (e e' : P ≃ᵃⁱ[𝕜] P) :

⇑(e * e') = ⇑e ∘ ⇑e'

@[simp]

theorem AffineIsometryEquiv.coe_inv {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (e : P ≃ᵃⁱ[𝕜] P) :

⇑e⁻¹ = ⇑e.symm

@[simp]

theorem AffineIsometryEquiv.map_vadd {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (p : P) (v : V) :

e (v +ᵥ p) = e.linearIsometryEquiv v +ᵥ e p

@[simp]

theorem AffineIsometryEquiv.map_vsub {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (p1 p2 : P) :

e.linearIsometryEquiv (p1 -ᵥ p2) = e p1 -ᵥ e p2

@[simp]

theorem AffineIsometryEquiv.dist_map {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x y : P) :

dist (e x) (e y) = dist x y

@[simp]

theorem AffineIsometryEquiv.edist_map {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x y : P) :

edist (e x) (e y) = edist x y

theorem AffineIsometryEquiv.bijective {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

Function.Bijective ⇑e

theorem AffineIsometryEquiv.injective {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

Function.Injective ⇑e

theorem AffineIsometryEquiv.surjective {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

Function.Surjective ⇑e

theorem AffineIsometryEquiv.map_eq_iff {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x y : P} :

e x = e y ↔ x = y

theorem AffineIsometryEquiv.map_ne {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {x y : P} (h : x ≠ y) :

e x ≠ e y

theorem AffineIsometryEquiv.lipschitz {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

LipschitzWith 1 ⇑e

theorem AffineIsometryEquiv.antilipschitz {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) :

AntilipschitzWith 1 ⇑e

@[simp]

theorem AffineIsometryEquiv.ediam_image {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (s : Set P) :

EMetric.diam (⇑e '' s) = EMetric.diam s

@[simp]

theorem AffineIsometryEquiv.diam_image {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (s : Set P) :

Metric.diam (⇑e '' s) = Metric.diam s

@[simp]

theorem AffineIsometryEquiv.comp_continuousOn_iff {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {α : Type u_14} [TopologicalSpace α] {f : α → P} {s : Set α} :

ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s

@[simp]

theorem AffineIsometryEquiv.comp_continuous_iff {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {α : Type u_14} [TopologicalSpace α] {f : α → P} :

Continuous (⇑e ∘ f) ↔ Continuous f

def AffineIsometryEquiv.ofTop {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s₁ : AffineSubspace 𝕜 P) [Nonempty ↥s₁] (h : s₁ = ⊤) :

↥s₁ ≃ᵃⁱ[𝕜] P

The identity equivalence of an affine subspace equal to ⊤ to the whole space.

Equations

AffineIsometryEquiv.ofTop s₁ h = { toAffineEquiv := (AffineEquiv.ofEq s₁ ⊤ h).trans (AffineSubspace.topEquiv 𝕜 V P), norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.ofTop_apply {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ : AffineSubspace 𝕜 P} [Nonempty ↥s₁] (h : s₁ = ⊤) (x : ↥s₁) :

(ofTop s₁ h) x = ↑x

@[simp]

theorem AffineIsometryEquiv.ofTop_symm_apply_coe {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ : AffineSubspace 𝕜 P} [Nonempty ↥s₁] (h : s₁ = ⊤) (x : P) :

↑((ofTop s₁ h).symm x) = x

def AffineIsometryEquiv.ofEq {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : AffineSubspace 𝕜 P) [Nonempty ↥s₁] [Nonempty ↥s₂] (h : s₁ = s₂) :

↥s₁ ≃ᵃⁱ[𝕜] ↥s₂

AffineEquiv.ofEq as an AffineIsometryEquiv.

Equations

AffineIsometryEquiv.ofEq s₁ s₂ h = { toAffineEquiv := AffineEquiv.ofEq s₁ s₂ h, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_ofEq_apply {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P} [Nonempty ↥s₁] [Nonempty ↥s₂] (h : s₁ = s₂) (x : ↥s₁) :

↑((ofEq s₁ s₂ h) x) = ↑x

@[simp]

theorem AffineIsometryEquiv.ofEq_symm {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P} [Nonempty ↥s₁] [Nonempty ↥s₂] (h : s₁ = s₂) :

(ofEq s₁ s₂ h).symm = ofEq s₂ s₁ ⋯

@[simp]

theorem AffineIsometryEquiv.ofEq_rfl {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s₁ : AffineSubspace 𝕜 P} [Nonempty ↥s₁] :

ofEq s₁ s₁ ⋯ = refl 𝕜 ↥s₁

def AffineIsometryEquiv.vaddConst (𝕜 : Type u_1) {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) :

V ≃ᵃⁱ[𝕜] P

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

Equations

AffineIsometryEquiv.vaddConst 𝕜 p = { toAffineEquiv := AffineEquiv.vaddConst 𝕜 p, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_vaddConst {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) :

⇑(vaddConst 𝕜 p) = fun (v : V) => v +ᵥ p

@[simp]

theorem AffineIsometryEquiv.coe_vaddConst' {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) :

⇑(AffineEquiv.vaddConst 𝕜 p) = fun (v : V) => v +ᵥ p

@[simp]

theorem AffineIsometryEquiv.coe_vaddConst_symm {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) :

⇑(vaddConst 𝕜 p).symm = fun (p' : P) => p' -ᵥ p

@[simp]

theorem AffineIsometryEquiv.vaddConst_toAffineEquiv {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) :

(vaddConst 𝕜 p).toAffineEquiv = AffineEquiv.vaddConst 𝕜 p

def AffineIsometryEquiv.constVSub (𝕜 : Type u_1) {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) :

P ≃ᵃⁱ[𝕜] V

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

Equations

AffineIsometryEquiv.constVSub 𝕜 p = { toAffineEquiv := AffineEquiv.constVSub 𝕜 p, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_constVSub {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) :

⇑(constVSub 𝕜 p) = fun (x : P) => p -ᵥ x

@[simp]

theorem AffineIsometryEquiv.symm_constVSub {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) :

(constVSub 𝕜 p).symm = (LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (vaddConst 𝕜 p)

def AffineIsometryEquiv.constVAdd (𝕜 : Type u_1) {V : Type u_2} (P : Type u_10) [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) :

P ≃ᵃⁱ[𝕜] P

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

Equations

AffineIsometryEquiv.constVAdd 𝕜 P v = { toAffineEquiv := AffineEquiv.constVAdd 𝕜 P v, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_constVAdd {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) :

⇑(constVAdd 𝕜 P v) = fun (x : P) => v +ᵥ x

@[simp]

theorem AffineIsometryEquiv.constVAdd_zero {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] :

constVAdd 𝕜 P 0 = refl 𝕜 P

theorem AffineIsometryEquiv.vadd_vsub {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] {f : P → P₂} (hf : Isometry f) {p : P} {g : V → V₂} (hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p) :

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

def AffineIsometryEquiv.pointReflection (𝕜 : Type u_1) {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :

P ≃ᵃⁱ[𝕜] P

Point reflection in x as an affine isometric automorphism.

Equations

AffineIsometryEquiv.pointReflection 𝕜 x = (AffineIsometryEquiv.constVSub 𝕜 x).trans (AffineIsometryEquiv.vaddConst 𝕜 x)

theorem AffineIsometryEquiv.pointReflection_apply {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) :

(pointReflection 𝕜 x) y = (x -ᵥ y) +ᵥ x

@[simp]

theorem AffineIsometryEquiv.pointReflection_toAffineEquiv {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :

(pointReflection 𝕜 x).toAffineEquiv = AffineEquiv.pointReflection 𝕜 x

@[simp]

theorem AffineIsometryEquiv.pointReflection_self {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :

(pointReflection 𝕜 x) x = x

theorem AffineIsometryEquiv.pointReflection_involutive {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :

Function.Involutive ⇑(pointReflection 𝕜 x)

@[simp]

theorem AffineIsometryEquiv.pointReflection_symm {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :

(pointReflection 𝕜 x).symm = pointReflection 𝕜 x

@[simp]

theorem AffineIsometryEquiv.dist_pointReflection_fixed {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) :

dist ((pointReflection 𝕜 x) y) x = dist y x

theorem AffineIsometryEquiv.dist_pointReflection_self' {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) :

dist ((pointReflection 𝕜 x) y) y = ‖2 • (x -ᵥ y)‖

theorem AffineIsometryEquiv.dist_pointReflection_self {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) :

dist ((pointReflection 𝕜 x) y) y = ‖2‖ * dist x y

theorem AffineIsometryEquiv.pointReflection_fixed_iff {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [Invertible 2] {x y : P} :

(pointReflection 𝕜 x) y = y ↔ y = x

theorem AffineIsometryEquiv.dist_pointReflection_self_real {V : Type u_2} {P : Type u_10} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [NormedSpace ℝ V] (x y : P) :

dist ((pointReflection ℝ x) y) y = 2 * dist x y

@[simp]

theorem AffineIsometryEquiv.pointReflection_midpoint_left {V : Type u_2} {P : Type u_10} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [NormedSpace ℝ V] (x y : P) :

(pointReflection ℝ (midpoint ℝ x y)) x = y

@[simp]

theorem AffineIsometryEquiv.pointReflection_midpoint_right {V : Type u_2} {P : Type u_10} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [NormedSpace ℝ V] (x y : P) :

(pointReflection ℝ (midpoint ℝ x y)) y = x

theorem AffineMap.continuous_linear_iff {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor 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.

theorem AffineMap.isOpenMap_linear_iff {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] {f : P →ᵃ[𝕜] P₂} :

IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

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

noncomputable def AffineSubspace.equivMapOfInjective {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁] [NormedSpace 𝕜 V₁] [PseudoMetricSpace P₁] [NormedAddTorsor V₁ P₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (E : AffineSubspace 𝕜 P₁) [Nonempty ↥E] (φ : P₁ →ᵃ[𝕜] P₂) (hφ : Function.Injective ⇑φ) :

↥E ≃ᵃ[𝕜] ↥(map φ E)

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem AffineSubspace.linear_equivMapOfInjective {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁] [NormedSpace 𝕜 V₁] [PseudoMetricSpace P₁] [NormedAddTorsor V₁ P₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (E : AffineSubspace 𝕜 P₁) [Nonempty ↥E] (φ : P₁ →ᵃ[𝕜] P₂) (hφ : Function.Injective ⇑φ) :

(E.equivMapOfInjective φ hφ).linear = (Submodule.equivMapOfInjective φ.linear ⋯ E.direction).trans (LinearEquiv.ofEq (Submodule.map φ.linear E.direction) (map φ E).direction ⋯)

@[simp]

theorem AffineSubspace.equivMapOfInjective_toFun {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁] [NormedSpace 𝕜 V₁] [PseudoMetricSpace P₁] [NormedAddTorsor V₁ P₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (E : AffineSubspace 𝕜 P₁) [Nonempty ↥E] (φ : P₁ →ᵃ[𝕜] P₂) (hφ : Function.Injective ⇑φ) (p : ↑↑E) :

(E.equivMapOfInjective φ hφ) p = ⟨φ ↑p, ⋯⟩

noncomputable def AffineSubspace.isometryEquivMap {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁'] [NormedSpace 𝕜 V₁'] [MetricSpace P₁'] [NormedAddTorsor V₁' P₁'] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁') [Nonempty ↥E] :

↥E ≃ᵃⁱ[𝕜] ↥(map φ.toAffineMap E)

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

This is an isometry version of AffineSubspace.equivMap, having a stronger premise and a stronger conclusion.

Equations

AffineSubspace.isometryEquivMap φ E = { toAffineEquiv := E.equivMapOfInjective φ.toAffineMap ⋯, norm_map := ⋯ }

@[simp]

theorem AffineSubspace.isometryEquivMap.apply_symm_apply {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁'] [NormedSpace 𝕜 V₁'] [MetricSpace P₁'] [NormedAddTorsor V₁' P₁'] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] {E : AffineSubspace 𝕜 P₁'} [Nonempty ↥E] {φ : P₁' →ᵃⁱ[𝕜] P₂} (x : ↥(map φ.toAffineMap E)) :

φ ↑((isometryEquivMap φ E).symm x) = ↑x

@[simp]

theorem AffineSubspace.isometryEquivMap.coe_apply {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁'] [NormedSpace 𝕜 V₁'] [MetricSpace P₁'] [NormedAddTorsor V₁' P₁'] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁') [Nonempty ↥E] (g : ↥E) :

↑((isometryEquivMap φ E) g) = φ ↑g

@[simp]

theorem AffineSubspace.isometryEquivMap.toAffineMap_eq {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁'] [NormedSpace 𝕜 V₁'] [MetricSpace P₁'] [NormedAddTorsor V₁' P₁'] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁') [Nonempty ↥E] :

↑(isometryEquivMap φ E).toAffineEquiv = ↑(E.equivMapOfInjective φ.toAffineMap ⋯)