Affine isometries #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define affine_isometry 𝕜 P P₂ to be an affine isometric embedding of normed
add-torsors P into P₂ over normed 𝕜-spaces and affine_isometry_equiv to be an affine
isometric equivalence between P and P₂.
We also prove basic lemmas and provide convenience constructors. The choice of these lemmas and
constructors is closely modelled on those for the linear_isometry and affine_map theories.
Since many elementary properties don't require ‖x‖ = 0 → x = 0 we initially set up the theory for
seminormed_add_comm_group and specialize to normed_add_comm_group only when needed.
Notation #
We introduce the notation P →ᵃⁱ[𝕜] P₂ for affine_isometry 𝕜 P P₂, and P ≃ᵃⁱ[𝕜] P₂ for
affine_isometry_equiv 𝕜 P P₂. In contrast with the notation →ₗᵢ for linear isometries, ≃ᵢ
for isometric equivalences, etc., the "i" here is a superscript. This is for aesthetic reasons to
match the superscript "a" (note that in mathlib →ᵃ is an affine map, since →ₐ has been taken by
algebra-homomorphisms.)
structure
affine_isometry
(𝕜 : Type u_1)
{V : Type u_2}
{V₂ : Type u_4}
(P : Type u_8)
(P₂ : Type u_9)
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂] :
Type (max u_2 u_4 u_8 u_9)
An 𝕜-affine isometric embedding of one normed add-torsor over a normed 𝕜-space into
another.
Instances for affine_isometry
- affine_isometry.has_sizeof_inst
- affine_isometry.has_coe_to_fun
- affine_isometry.inhabited
- affine_isometry.monoid
@[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₂) :
The underlying linear map of an affine isometry is in fact a linear isometry.
Equations
- f.linear_isometry = {to_linear_map := {to_fun := f.to_affine_map.linear.to_fun, map_add' := _, map_smul' := _}, norm_map' := _}
@[simp]
theorem
affine_isometry.linear_eq_linear_isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂) :
@[protected, instance]
def
affine_isometry.has_coe_to_fun
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂] :
Equations
- affine_isometry.has_coe_to_fun = {coe := λ (f : P →ᵃⁱ[𝕜] P₂), f.to_affine_map.to_fun}
@[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
theorem
affine_isometry.to_affine_map_injective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂] :
theorem
affine_isometry.coe_fn_injective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂] :
@[ext]
theorem
affine_isometry.ext
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
{f g : P →ᵃⁱ[𝕜] P₂}
(h : ∀ (x : P), ⇑f x = ⇑g x) :
f = g
def
linear_isometry.to_affine_isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
(f : V →ₗᵢ[𝕜] V₂) :
Reinterpret a linear isometry as an affine isometry.
Equations
- f.to_affine_isometry = {to_affine_map := {to_fun := f.to_linear_map.to_affine_map.to_fun, linear := f.to_linear_map.to_affine_map.linear, map_vadd' := _}, norm_map := _}
@[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
@[simp]
theorem
linear_isometry.to_affine_isometry_linear_isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
(f : V →ₗᵢ[𝕜] V₂) :
@[simp]
theorem
linear_isometry.to_affine_isometry_to_affine_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
(f : V →ₗᵢ[𝕜] V₂) :
@[simp]
theorem
affine_isometry.map_vadd
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(p : P)
(v : V) :
@[simp]
theorem
affine_isometry.map_vsub
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(p1 p2 : P) :
@[simp]
theorem
affine_isometry.dist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(x y : P) :
has_dist.dist (⇑f x) (⇑f y) = has_dist.dist x y
@[simp]
theorem
affine_isometry.nndist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[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
@[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
@[protected]
theorem
affine_isometry.isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂) :
@[protected]
theorem
affine_isometry.injective
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(f₁ : P₁ →ᵃⁱ[𝕜] P₂) :
@[simp]
theorem
affine_isometry.map_eq_iff
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(f₁ : P₁ →ᵃⁱ[𝕜] P₂)
{x y : P₁} :
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) :
@[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
@[protected]
theorem
affine_isometry.antilipschitz
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂) :
@[protected, continuity]
theorem
affine_isometry.continuous
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂) :
theorem
affine_isometry.ediam_image
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(s : set P) :
emetric.diam (⇑f '' s) = emetric.diam s
theorem
affine_isometry.ediam_range
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂) :
theorem
affine_isometry.diam_image
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(s : set P) :
metric.diam (⇑f '' s) = metric.diam s
theorem
affine_isometry.diam_range
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂) :
@[simp]
theorem
affine_isometry.comp_continuous_iff
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
{α : Type u_3}
[topological_space α]
{g : α → P} :
continuous (⇑f ∘ g) ↔ continuous g
def
affine_isometry.id
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
The identity affine isometry.
Equations
@[simp]
theorem
affine_isometry.coe_id
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
@[simp]
theorem
affine_isometry.id_apply
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x : P) :
⇑affine_isometry.id x = x
@[simp]
theorem
affine_isometry.id_to_affine_map
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
@[protected, instance]
def
affine_isometry.inhabited
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
Equations
- affine_isometry.inhabited = {default := affine_isometry.id _inst_17}
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₂) :
Composition of affine isometries.
Equations
- g.comp f = {to_affine_map := g.to_affine_map.comp f.to_affine_map, norm_map := _}
@[simp]
theorem
affine_isometry.coe_comp
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{V₃ : Type u_5}
{P : Type u_8}
{P₂ : Type u_9}
{P₃ : Type u_10}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[normed_space 𝕜 V₃]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[pseudo_metric_space P₃]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
[normed_add_torsor V₃ P₃]
(g : P₂ →ᵃⁱ[𝕜] P₃)
(f : P →ᵃⁱ[𝕜] P₂) :
@[simp]
theorem
affine_isometry.id_comp
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂) :
affine_isometry.id.comp f = f
@[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
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₂) :
@[protected, instance]
def
affine_isometry.monoid
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
Equations
- affine_isometry.monoid = {mul := affine_isometry.comp _inst_17, mul_assoc := _, one := affine_isometry.id _inst_17, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (P →ᵃⁱ[𝕜] P)), npow_zero' := _, npow_succ' := _}
@[simp]
theorem
affine_isometry.coe_one
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
@[simp]
theorem
affine_isometry.coe_mul
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(f g : P →ᵃⁱ[𝕜] P) :
def
affine_subspace.subtypeₐᵢ
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace 𝕜 P)
[nonempty ↥s] :
theorem
affine_subspace.subtypeₐᵢ_linear
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace 𝕜 P)
[nonempty ↥s] :
@[simp]
theorem
affine_subspace.subtypeₐᵢ_linear_isometry
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace 𝕜 P)
[nonempty ↥s] :
@[simp]
theorem
affine_subspace.coe_subtypeₐᵢ
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace 𝕜 P)
[nonempty ↥s] :
@[simp]
theorem
affine_subspace.subtypeₐᵢ_to_affine_map
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace 𝕜 P)
[nonempty ↥s] :
structure
affine_isometry_equiv
(𝕜 : Type u_1)
{V : Type u_2}
{V₂ : Type u_4}
(P : Type u_8)
(P₂ : Type u_9)
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂] :
Type (max u_2 u_4 u_8 u_9)
A affine isometric equivalence between two normed vector spaces.
Instances for affine_isometry_equiv
- affine_isometry_equiv.has_sizeof_inst
- affine_isometry_equiv.has_coe_to_fun
- affine_isometry_equiv.inhabited
- affine_isometry_equiv.group
@[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₂) :
The underlying linear equiv of an affine isometry equiv is in fact a linear isometry equiv.
Equations
- e.linear_isometry_equiv = {to_linear_equiv := {to_fun := e.to_affine_equiv.linear.to_fun, map_add' := _, map_smul' := _, inv_fun := e.to_affine_equiv.linear.inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
affine_isometry_equiv.linear_eq_linear_isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected, instance]
def
affine_isometry_equiv.has_coe_to_fun
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂] :
Equations
- affine_isometry_equiv.has_coe_to_fun = {coe := λ (f : P ≃ᵃⁱ[𝕜] P₂), f.to_affine_equiv.to_equiv.to_fun}
@[simp]
theorem
affine_isometry_equiv.coe_mk
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃ[𝕜] P₂)
(he : ∀ (x : V), ‖⇑(e.linear) x‖ = ‖x‖) :
@[simp]
theorem
affine_isometry_equiv.coe_to_affine_equiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
⇑(e.to_affine_equiv) = ⇑e
theorem
affine_isometry_equiv.to_affine_equiv_injective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂] :
@[ext]
theorem
affine_isometry_equiv.ext
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
{e e' : P ≃ᵃⁱ[𝕜] P₂}
(h : ∀ (x : P), ⇑e x = ⇑e' x) :
e = e'
def
affine_isometry_equiv.to_affine_isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
Reinterpret a affine_isometry_equiv as a affine_isometry.
Equations
- e.to_affine_isometry = {to_affine_map := e.to_affine_equiv.to_affine_map, norm_map := _}
@[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
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) :
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
- affine_isometry_equiv.mk' e e' p h = {to_affine_equiv := {to_equiv := (affine_equiv.mk' e e'.to_linear_equiv p h).to_equiv, linear := (affine_equiv.mk' e e'.to_linear_equiv p h).linear, map_vadd' := _}, norm_map := _}
@[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
@[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'
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₂) :
Reinterpret a linear isometry equiv as an affine isometry equiv.
Equations
- e.to_affine_isometry_equiv = {to_affine_equiv := {to_equiv := e.to_linear_equiv.to_affine_equiv.to_equiv, linear := e.to_linear_equiv.to_affine_equiv.linear, map_vadd' := _}, norm_map := _}
@[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
@[simp]
theorem
linear_isometry_equiv.to_affine_isometry_equiv_linear_isometry_equiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
(e : V ≃ₗᵢ[𝕜] V₂) :
@[simp]
theorem
linear_isometry_equiv.to_affine_isometry_equiv_to_affine_equiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
(e : V ≃ₗᵢ[𝕜] V₂) :
@[simp]
theorem
linear_isometry_equiv.to_affine_isometry_equiv_to_affine_isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
(e : V ≃ₗᵢ[𝕜] V₂) :
@[protected]
theorem
affine_isometry_equiv.isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
def
affine_isometry_equiv.to_isometry_equiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
P ≃ᵢ P₂
Reinterpret a affine_isometry_equiv as an isometry_equiv.
Equations
- e.to_isometry_equiv = {to_equiv := e.to_affine_equiv.to_equiv, isometry_to_fun := _}
@[simp]
theorem
affine_isometry_equiv.coe_to_isometry_equiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
⇑(e.to_isometry_equiv) = ⇑e
theorem
affine_isometry_equiv.range_eq_univ
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
def
affine_isometry_equiv.to_homeomorph
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
P ≃ₜ P₂
Reinterpret a affine_isometry_equiv as an homeomorph.
Equations
@[simp]
theorem
affine_isometry_equiv.coe_to_homeomorph
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
⇑(e.to_homeomorph) = ⇑e
@[protected]
theorem
affine_isometry_equiv.continuous
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected]
theorem
affine_isometry_equiv.continuous_at
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
{x : P} :
continuous_at ⇑e x
@[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
@[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
def
affine_isometry_equiv.refl
(𝕜 : Type u_1)
{V : Type u_2}
(P : Type u_8)
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
Identity map as a affine_isometry_equiv.
Equations
@[protected, instance]
def
affine_isometry_equiv.inhabited
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
Equations
- affine_isometry_equiv.inhabited = {default := affine_isometry_equiv.refl 𝕜 P _inst_17}
@[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
@[simp]
theorem
affine_isometry_equiv.to_affine_equiv_refl
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
@[simp]
theorem
affine_isometry_equiv.to_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] :
@[simp]
theorem
affine_isometry_equiv.to_homeomorph_refl
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
def
affine_isometry_equiv.symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
The inverse affine_isometry_equiv.
Equations
- e.symm = {to_affine_equiv := {to_equiv := e.to_affine_equiv.symm.to_equiv, linear := e.to_affine_equiv.symm.linear, map_vadd' := _}, norm_map := _}
@[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₂) :
@[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) :
@[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₂) :
@[simp]
theorem
affine_isometry_equiv.to_affine_equiv_symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
@[simp]
theorem
affine_isometry_equiv.to_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₂) :
@[simp]
theorem
affine_isometry_equiv.to_homeomorph_symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
def
affine_isometry_equiv.trans
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{V₃ : Type u_5}
{P : Type u_8}
{P₂ : Type u_9}
{P₃ : Type u_10}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[normed_space 𝕜 V₃]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[pseudo_metric_space P₃]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
[normed_add_torsor V₃ P₃]
(e : P ≃ᵃⁱ[𝕜] P₂)
(e' : P₂ ≃ᵃⁱ[𝕜] P₃) :
Composition of affine_isometry_equivs as a affine_isometry_equiv.
Equations
- e.trans e' = {to_affine_equiv := e.to_affine_equiv.trans e'.to_affine_equiv, norm_map := _}
@[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₃) :
@[simp]
theorem
affine_isometry_equiv.trans_refl
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
e.trans (affine_isometry_equiv.refl 𝕜 P₂) = e
@[simp]
theorem
affine_isometry_equiv.refl_trans
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
(affine_isometry_equiv.refl 𝕜 P).trans e = e
@[simp]
theorem
affine_isometry_equiv.self_trans_symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[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
@[simp]
theorem
affine_isometry_equiv.symm_trans_self
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
e.symm.trans e = affine_isometry_equiv.refl 𝕜 P₂
@[simp]
theorem
affine_isometry_equiv.coe_symm_trans
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{V₃ : Type u_5}
{P : Type u_8}
{P₂ : Type u_9}
{P₃ : Type u_10}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[normed_space 𝕜 V₃]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[pseudo_metric_space P₃]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
[normed_add_torsor V₃ P₃]
(e₁ : P ≃ᵃⁱ[𝕜] P₂)
(e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) :
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₄) :
@[protected, instance]
def
affine_isometry_equiv.group
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
The group of affine isometries of a normed_add_torsor, P.
Equations
- affine_isometry_equiv.group = {mul := λ (e₁ e₂ : P ≃ᵃⁱ[𝕜] P), e₂.trans e₁, mul_assoc := _, one := affine_isometry_equiv.refl 𝕜 P _inst_17, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (affine_isometry_equiv.refl 𝕜 P) (λ (e₁ e₂ : P ≃ᵃⁱ[𝕜] P), e₂.trans e₁) affine_isometry_equiv.trans_refl affine_isometry_equiv.refl_trans, npow_zero' := _, npow_succ' := _, inv := affine_isometry_equiv.symm _inst_17, div := div_inv_monoid.div._default (λ (e₁ e₂ : P ≃ᵃⁱ[𝕜] P), e₂.trans e₁) affine_isometry_equiv.group._proof_4 (affine_isometry_equiv.refl 𝕜 P) affine_isometry_equiv.trans_refl affine_isometry_equiv.refl_trans (div_inv_monoid.npow._default (affine_isometry_equiv.refl 𝕜 P) (λ (e₁ e₂ : P ≃ᵃⁱ[𝕜] P), e₂.trans e₁) affine_isometry_equiv.trans_refl affine_isometry_equiv.refl_trans) affine_isometry_equiv.group._proof_5 affine_isometry_equiv.group._proof_6 affine_isometry_equiv.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (e₁ e₂ : P ≃ᵃⁱ[𝕜] P), e₂.trans e₁) affine_isometry_equiv.group._proof_8 (affine_isometry_equiv.refl 𝕜 P) affine_isometry_equiv.trans_refl affine_isometry_equiv.refl_trans (div_inv_monoid.npow._default (affine_isometry_equiv.refl 𝕜 P) (λ (e₁ e₂ : P ≃ᵃⁱ[𝕜] P), e₂.trans e₁) affine_isometry_equiv.trans_refl affine_isometry_equiv.refl_trans) affine_isometry_equiv.group._proof_9 affine_isometry_equiv.group._proof_10 affine_isometry_equiv.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem
affine_isometry_equiv.coe_one
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
@[simp]
theorem
affine_isometry_equiv.coe_mul
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(e e' : P ≃ᵃⁱ[𝕜] P) :
@[simp]
theorem
affine_isometry_equiv.coe_inv
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(e : P ≃ᵃⁱ[𝕜] P) :
@[simp]
theorem
affine_isometry_equiv.map_vadd
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(p : P)
(v : V) :
@[simp]
theorem
affine_isometry_equiv.map_vsub
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(p1 p2 : P) :
@[simp]
theorem
affine_isometry_equiv.dist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(x y : P) :
has_dist.dist (⇑e x) (⇑e y) = has_dist.dist x y
@[simp]
theorem
affine_isometry_equiv.edist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[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
@[protected]
theorem
affine_isometry_equiv.bijective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected]
theorem
affine_isometry_equiv.injective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
@[protected]
theorem
affine_isometry_equiv.surjective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
@[simp]
theorem
affine_isometry_equiv.map_eq_iff
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
{x y : P} :
theorem
affine_isometry_equiv.map_ne
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
{x y : P}
(h : x ≠ y) :
@[protected]
theorem
affine_isometry_equiv.lipschitz
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
lipschitz_with 1 ⇑e
@[protected]
theorem
affine_isometry_equiv.antilipschitz
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂) :
@[simp]
theorem
affine_isometry_equiv.ediam_image
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(s : set P) :
emetric.diam (⇑e '' s) = emetric.diam s
@[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
@[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
@[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
def
affine_isometry_equiv.vadd_const
(𝕜 : Type u_1)
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(p : P) :
The map v ↦ v +ᵥ p as an affine isometric equivalence between V and P.
Equations
- affine_isometry_equiv.vadd_const 𝕜 p = {to_affine_equiv := {to_equiv := (affine_equiv.vadd_const 𝕜 p).to_equiv, linear := (affine_equiv.vadd_const 𝕜 p).linear, map_vadd' := _}, norm_map := _}
@[simp]
theorem
affine_isometry_equiv.coe_vadd_const
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(p : P) :
⇑(affine_isometry_equiv.vadd_const 𝕜 p) = λ (v : V), v +ᵥ p
@[simp]
theorem
affine_isometry_equiv.coe_vadd_const_symm
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(p : P) :
⇑((affine_isometry_equiv.vadd_const 𝕜 p).symm) = λ (p' : P), p' -ᵥ p
@[simp]
theorem
affine_isometry_equiv.vadd_const_to_affine_equiv
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(p : P) :
def
affine_isometry_equiv.const_vsub
(𝕜 : Type u_1)
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(p : P) :
p' ↦ p -ᵥ p' as an affine isometric equivalence.
Equations
- affine_isometry_equiv.const_vsub 𝕜 p = {to_affine_equiv := {to_equiv := (affine_equiv.const_vsub 𝕜 p).to_equiv, linear := (affine_equiv.const_vsub 𝕜 p).linear, map_vadd' := _}, norm_map := _}
@[simp]
theorem
affine_isometry_equiv.coe_const_vsub
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(p : P) :
@[simp]
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) :
def
affine_isometry_equiv.const_vadd
(𝕜 : Type u_1)
{V : Type u_2}
(P : Type u_8)
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(v : V) :
Translation by v (that is, the map p ↦ v +ᵥ p) as an affine isometric automorphism of P.
Equations
- affine_isometry_equiv.const_vadd 𝕜 P v = {to_affine_equiv := {to_equiv := (affine_equiv.const_vadd 𝕜 P v).to_equiv, linear := (affine_equiv.const_vadd 𝕜 P v).linear, map_vadd' := _}, norm_map := _}
@[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
@[simp]
theorem
affine_isometry_equiv.const_vadd_zero
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
theorem
affine_isometry_equiv.vadd_vsub
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V]
[normed_space 𝕜 V₂]
[pseudo_metric_space P]
[pseudo_metric_space P₂]
[normed_add_torsor V P]
[normed_add_torsor V₂ P₂]
{f : P → P₂}
(hf : isometry f)
{p : P}
{g : V → V₂}
(hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p) :
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.
def
affine_isometry_equiv.point_reflection
(𝕜 : Type u_1)
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x : P) :
Point reflection in x as an affine isometric automorphism.
Equations
theorem
affine_isometry_equiv.point_reflection_apply
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x y : P) :
⇑(affine_isometry_equiv.point_reflection 𝕜 x) y = x -ᵥ y +ᵥ x
@[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) :
@[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
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) :
@[simp]
theorem
affine_isometry_equiv.point_reflection_symm
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x : P) :
@[simp]
theorem
affine_isometry_equiv.dist_point_reflection_fixed
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[normed_field 𝕜]
[seminormed_add_comm_group V]
[normed_space 𝕜 V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x y : P) :
has_dist.dist (⇑(affine_isometry_equiv.point_reflection 𝕜 x) y) x = has_dist.dist y x
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)‖
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
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
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
@[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) :
@[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) :
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.
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.
@[simp]
theorem
affine_subspace.equiv_map_of_injective_apply
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(E : affine_subspace 𝕜 P₁)
[nonempty ↥E]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : function.injective ⇑φ)
(ᾰ : ↥↑E) :
⇑(E.equiv_map_of_injective φ hφ) ᾰ = (equiv.set.image ⇑φ ↑E hφ).to_fun ᾰ
@[simp]
theorem
affine_subspace.linear_equiv_map_of_injective
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(E : affine_subspace 𝕜 P₁)
[nonempty ↥E]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : function.injective ⇑φ) :
(E.equiv_map_of_injective φ hφ).linear = (submodule.equiv_map_of_injective φ.linear _ E.direction).trans (linear_equiv.of_eq (submodule.map φ.linear E.direction) (affine_subspace.map φ E).direction _)
noncomputable
def
affine_subspace.equiv_map_of_injective
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(E : affine_subspace 𝕜 P₁)
[nonempty ↥E]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : function.injective ⇑φ) :
↥E ≃ᵃ[𝕜] ↥(affine_subspace.map φ E)
An affine subspace is isomorphic to its image under an injective affine map.
This is the affine version of submodule.equiv_map_of_injective.
Equations
- E.equiv_map_of_injective φ hφ = {to_equiv := {to_fun := (equiv.set.image ⇑φ ↑E hφ).to_fun, inv_fun := (equiv.set.image ⇑φ ↑E hφ).inv_fun, left_inv := _, right_inv := _}, linear := (submodule.equiv_map_of_injective φ.linear _ E.direction).trans (linear_equiv.of_eq (submodule.map φ.linear E.direction) (affine_subspace.map φ E).direction _), map_vadd' := _}
@[simp]
theorem
affine_subspace.equiv_map_of_injective_symm_apply
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(E : affine_subspace 𝕜 P₁)
[nonempty ↥E]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : function.injective ⇑φ)
(ᾰ : ↥(⇑φ '' ↑E)) :
⇑((E.equiv_map_of_injective φ hφ).symm) ᾰ = (equiv.set.image ⇑φ ↑E hφ).inv_fun ᾰ
noncomputable
def
affine_subspace.isometry_equiv_map
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(φ : P₁ →ᵃⁱ[𝕜] P₂)
(E : affine_subspace 𝕜 P₁)
[nonempty ↥E] :
↥E ≃ᵃⁱ[𝕜] ↥(affine_subspace.map φ.to_affine_map E)
Restricts an affine isometry to an affine isometry equivalence between a nonempty affine
subspace E and its image.
This is an isometry version of affine_subspace.equiv_map, having a stronger premise and a stronger
conclusion.
Equations
- affine_subspace.isometry_equiv_map φ E = {to_affine_equiv := E.equiv_map_of_injective φ.to_affine_map _, norm_map := _}
@[simp]
theorem
affine_subspace.isometry_equiv_map.apply_symm_apply
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
{E : affine_subspace 𝕜 P₁}
[nonempty ↥E]
{φ : P₁ →ᵃⁱ[𝕜] P₂}
(x : ↥(affine_subspace.map φ.to_affine_map E)) :
@[simp]
theorem
affine_subspace.isometry_equiv_map.coe_apply
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(φ : P₁ →ᵃⁱ[𝕜] P₂)
(E : affine_subspace 𝕜 P₁)
[nonempty ↥E]
(g : ↥E) :
@[simp]
theorem
affine_subspace.isometry_equiv_map.to_affine_map_eq
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[normed_field 𝕜]
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[normed_space 𝕜 V₁]
[normed_space 𝕜 V₂]
[metric_space P₁]
[pseudo_metric_space P₂]
[normed_add_torsor V₁ P₁]
[normed_add_torsor V₂ P₂]
(φ : P₁ →ᵃⁱ[𝕜] P₂)
(E : affine_subspace 𝕜 P₁)
[nonempty ↥E] :