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_4}
(P : Type u_8)
(P₂ : Type u_9)
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
extends
AffineMap
:
Type (max (max (max u_2 u_4) u_8) u_9)
- toFun : P → P₂
- map_vadd' : ∀ (p : P) (v : V), AffineMap.toFun s.toAffineMap (v +ᵥ p) = ↑s.linear v +ᵥ AffineMap.toFun s.toAffineMap p
A 𝕜-affine isometric embedding of one normed add-torsor over a normed 𝕜-space into
another.
Instances For
def
AffineIsometry.linearIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
The underlying linear map of an affine isometry is in fact a linear isometry.
Instances For
@[simp]
theorem
AffineIsometry.linear_eq_linearIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
f.linear = (AffineIsometry.linearIsometry f).toLinearMap
instance
AffineIsometry.instFunLikeAffineIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
:
@[simp]
theorem
AffineIsometry.coe_toAffineMap
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
↑f.toAffineMap = ↑f
theorem
AffineIsometry.toAffineMap_injective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
:
Function.Injective AffineIsometry.toAffineMap
theorem
AffineIsometry.coeFn_injective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
:
Function.Injective FunLike.coe
theorem
AffineIsometry.ext
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
{f : P →ᵃⁱ[𝕜] P₂}
{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_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(f : V →ₗᵢ[𝕜] V₂)
:
Reinterpret a linear isometry as an affine isometry.
Instances For
@[simp]
theorem
LinearIsometry.coe_toAffineIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(f : V →ₗᵢ[𝕜] V₂)
:
↑(LinearIsometry.toAffineIsometry f) = ↑f
@[simp]
theorem
LinearIsometry.toAffineIsometry_linearIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(f : V →ₗᵢ[𝕜] V₂)
:
@[simp]
theorem
LinearIsometry.toAffineIsometry_toAffineMap
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(f : V →ₗᵢ[𝕜] V₂)
:
(LinearIsometry.toAffineIsometry f).toAffineMap = LinearMap.toAffineMap f.toLinearMap
@[simp]
theorem
AffineIsometry.map_vadd
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(p : P)
(v : V)
:
↑f (v +ᵥ p) = ↑(AffineIsometry.linearIsometry f) v +ᵥ ↑f p
@[simp]
theorem
AffineIsometry.map_vsub
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(p1 : P)
(p2 : P)
:
↑(AffineIsometry.linearIsometry f) (p1 -ᵥ p2) = ↑f p1 -ᵥ ↑f p2
@[simp]
theorem
AffineIsometry.dist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(x : P)
(y : P)
:
@[simp]
theorem
AffineIsometry.nndist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(x : P)
(y : P)
:
@[simp]
theorem
AffineIsometry.edist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
(x : P)
(y : P)
:
theorem
AffineIsometry.isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
Isometry ↑f
theorem
AffineIsometry.injective
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(f₁ : P₁ →ᵃⁱ[𝕜] P₂)
:
@[simp]
theorem
AffineIsometry.map_eq_iff
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(f₁ : P₁ →ᵃⁱ[𝕜] P₂)
{x : P₁}
{y : P₁}
:
theorem
AffineIsometry.map_ne
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(f₁ : P₁ →ᵃⁱ[𝕜] P₂)
{x : P₁}
{y : P₁}
(h : x ≠ y)
:
↑f₁ x ≠ ↑f₁ y
theorem
AffineIsometry.lipschitz
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
LipschitzWith 1 ↑f
theorem
AffineIsometry.antilipschitz
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
AntilipschitzWith 1 ↑f
theorem
AffineIsometry.continuous
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
Continuous ↑f
theorem
AffineIsometry.ediam_image
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
{α : Type u_12}
[TopologicalSpace α]
{g : α → P}
:
Continuous (↑f ∘ g) ↔ Continuous g
def
AffineIsometry.id
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
The identity affine isometry.
Instances For
@[simp]
theorem
AffineIsometry.coe_id
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
↑AffineIsometry.id = id
@[simp]
theorem
AffineIsometry.id_apply
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
:
↑AffineIsometry.id x = x
@[simp]
theorem
AffineIsometry.id_toAffineMap
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
AffineIsometry.id.toAffineMap = AffineMap.id 𝕜 P
instance
AffineIsometry.instInhabitedAffineIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
def
AffineIsometry.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}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[SeminormedAddCommGroup V₃]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[NormedSpace 𝕜 V₃]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[PseudoMetricSpace P₃]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
[NormedAddTorsor V₃ P₃]
(g : P₂ →ᵃⁱ[𝕜] P₃)
(f : P →ᵃⁱ[𝕜] P₂)
:
Composition of affine isometries.
Instances For
@[simp]
theorem
AffineIsometry.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}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[SeminormedAddCommGroup V₃]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[NormedSpace 𝕜 V₃]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[PseudoMetricSpace P₃]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
[NormedAddTorsor V₃ P₃]
(g : P₂ →ᵃⁱ[𝕜] P₃)
(f : P →ᵃⁱ[𝕜] P₂)
:
↑(AffineIsometry.comp g f) = ↑g ∘ ↑f
@[simp]
theorem
AffineIsometry.id_comp
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
AffineIsometry.comp AffineIsometry.id f = f
@[simp]
theorem
AffineIsometry.comp_id
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(f : P →ᵃⁱ[𝕜] P₂)
:
AffineIsometry.comp f AffineIsometry.id = f
theorem
AffineIsometry.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}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[SeminormedAddCommGroup V₃]
[SeminormedAddCommGroup V₄]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[NormedSpace 𝕜 V₃]
[NormedSpace 𝕜 V₄]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[PseudoMetricSpace P₃]
[PseudoMetricSpace P₄]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
[NormedAddTorsor V₃ P₃]
[NormedAddTorsor V₄ P₄]
(f : P₃ →ᵃⁱ[𝕜] P₄)
(g : P₂ →ᵃⁱ[𝕜] P₃)
(h : P →ᵃⁱ[𝕜] P₂)
:
AffineIsometry.comp (AffineIsometry.comp f g) h = AffineIsometry.comp f (AffineIsometry.comp g h)
instance
AffineIsometry.instMonoidAffineIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
@[simp]
theorem
AffineIsometry.coe_one
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
↑1 = id
@[simp]
theorem
AffineIsometry.coe_mul
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(f : P →ᵃⁱ[𝕜] P)
(g : P →ᵃⁱ[𝕜] P)
:
def
AffineSubspace.subtypeₐᵢ
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace 𝕜 P)
[Nonempty { x // x ∈ s }]
:
AffineSubspace.subtype as an AffineIsometry.
Instances For
theorem
AffineSubspace.subtypeₐᵢ_linear
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace 𝕜 P)
[Nonempty { x // x ∈ s }]
:
(AffineSubspace.subtypeₐᵢ s).toAffineMap.linear = Submodule.subtype (AffineSubspace.direction s)
@[simp]
theorem
AffineSubspace.subtypeₐᵢ_linearIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace 𝕜 P)
[Nonempty { x // x ∈ s }]
:
@[simp]
theorem
AffineSubspace.coe_subtypeₐᵢ
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace 𝕜 P)
[Nonempty { x // x ∈ s }]
:
↑(AffineSubspace.subtypeₐᵢ s) = ↑(AffineSubspace.subtype s)
@[simp]
theorem
AffineSubspace.subtypeₐᵢ_toAffineMap
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(s : AffineSubspace 𝕜 P)
[Nonempty { x // x ∈ s }]
:
(AffineSubspace.subtypeₐᵢ s).toAffineMap = AffineSubspace.subtype s
structure
AffineIsometryEquiv
(𝕜 : Type u_1)
{V : Type u_2}
{V₂ : Type u_4}
(P : Type u_8)
(P₂ : Type u_9)
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
extends
AffineEquiv
:
Type (max (max (max u_2 u_4) u_8) u_9)
- toFun : P → P₂
- invFun : P₂ → P
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
An affine isometric equivalence between two normed vector spaces.
Instances For
def
AffineIsometryEquiv.linearIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
The underlying linear equiv of an affine isometry equiv is in fact a linear isometry equiv.
Instances For
@[simp]
theorem
AffineIsometryEquiv.linear_eq_linear_isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
e.linear = (AffineIsometryEquiv.linearIsometryEquiv e).toLinearEquiv
instance
AffineIsometryEquiv.instEquivLikeAffineIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
:
@[simp]
theorem
AffineIsometryEquiv.coe_mk
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
↑e.toAffineEquiv = ↑e
theorem
AffineIsometryEquiv.toAffineEquiv_injective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
:
Function.Injective AffineIsometryEquiv.toAffineEquiv
theorem
AffineIsometryEquiv.ext
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
{e : P ≃ᵃⁱ[𝕜] P₂}
{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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
Reinterpret an AffineIsometryEquiv as an AffineIsometry.
Instances For
@[simp]
theorem
AffineIsometryEquiv.coe_toAffineIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
def
AffineIsometryEquiv.mk'
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor 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.
Instances For
@[simp]
theorem
AffineIsometryEquiv.coe_mk'
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(e : P₁ → P₂)
(e' : V₁ ≃ₗᵢ[𝕜] V₂)
(p : P₁)
(h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p)
:
↑(AffineIsometryEquiv.mk' e e' p h) = e
@[simp]
theorem
AffineIsometryEquiv.linearIsometryEquiv_mk'
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(e : P₁ → P₂)
(e' : V₁ ≃ₗᵢ[𝕜] V₂)
(p : P₁)
(h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p)
:
AffineIsometryEquiv.linearIsometryEquiv (AffineIsometryEquiv.mk' e e' p h) = e'
def
LinearIsometryEquiv.toAffineIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(e : V ≃ₗᵢ[𝕜] V₂)
:
Reinterpret a linear isometry equiv as an affine isometry equiv.
Instances For
@[simp]
theorem
LinearIsometryEquiv.coe_toAffineIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(e : V ≃ₗᵢ[𝕜] V₂)
:
@[simp]
theorem
LinearIsometryEquiv.toAffineIsometryEquiv_linearIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(e : V ≃ₗᵢ[𝕜] V₂)
:
@[simp]
theorem
LinearIsometryEquiv.toAffineIsometryEquiv_toAffineEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(e : V ≃ₗᵢ[𝕜] V₂)
:
(LinearIsometryEquiv.toAffineIsometryEquiv e).toAffineEquiv = LinearEquiv.toAffineEquiv e.toLinearEquiv
@[simp]
theorem
LinearIsometryEquiv.toAffineIsometryEquiv_toAffineIsometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
(e : V ≃ₗᵢ[𝕜] V₂)
:
theorem
AffineIsometryEquiv.isometry
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
Isometry ↑e
def
AffineIsometryEquiv.toIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
P ≃ᵢ P₂
Reinterpret an AffineIsometryEquiv as an IsometryEquiv.
Instances For
@[simp]
theorem
AffineIsometryEquiv.coe_toIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
↑(AffineIsometryEquiv.toIsometryEquiv e) = ↑e
theorem
AffineIsometryEquiv.range_eq_univ
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
def
AffineIsometryEquiv.toHomeomorph
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
P ≃ₜ P₂
Reinterpret an AffineIsometryEquiv as a Homeomorph.
Instances For
@[simp]
theorem
AffineIsometryEquiv.coe_toHomeomorph
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
↑(AffineIsometryEquiv.toHomeomorph e) = ↑e
theorem
AffineIsometryEquiv.continuous
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
Continuous ↑e
theorem
AffineIsometryEquiv.continuousAt
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_8)
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
Identity map as an AffineIsometryEquiv.
Instances For
instance
AffineIsometryEquiv.instInhabitedAffineIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
@[simp]
theorem
AffineIsometryEquiv.coe_refl
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
↑(AffineIsometryEquiv.refl 𝕜 P) = id
@[simp]
theorem
AffineIsometryEquiv.toAffineEquiv_refl
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
(AffineIsometryEquiv.refl 𝕜 P).toAffineEquiv = AffineEquiv.refl 𝕜 P
@[simp]
theorem
AffineIsometryEquiv.toIsometryEquiv_refl
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
@[simp]
theorem
AffineIsometryEquiv.toHomeomorph_refl
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
def
AffineIsometryEquiv.symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
The inverse AffineIsometryEquiv.
Instances For
@[simp]
theorem
AffineIsometryEquiv.apply_symm_apply
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(x : P₂)
:
↑e (↑(AffineIsometryEquiv.symm e) x) = x
@[simp]
theorem
AffineIsometryEquiv.symm_apply_apply
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(x : P)
:
↑(AffineIsometryEquiv.symm e) (↑e x) = x
@[simp]
theorem
AffineIsometryEquiv.symm_symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
@[simp]
theorem
AffineIsometryEquiv.toAffineEquiv_symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
AffineEquiv.symm e.toAffineEquiv = (AffineIsometryEquiv.symm e).toAffineEquiv
@[simp]
theorem
AffineIsometryEquiv.toIsometryEquiv_symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
@[simp]
theorem
AffineIsometryEquiv.toHomeomorph_symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
def
AffineIsometryEquiv.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}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[SeminormedAddCommGroup V₃]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[NormedSpace 𝕜 V₃]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[PseudoMetricSpace P₃]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
[NormedAddTorsor V₃ P₃]
(e : P ≃ᵃⁱ[𝕜] P₂)
(e' : P₂ ≃ᵃⁱ[𝕜] P₃)
:
Composition of AffineIsometryEquivs as an AffineIsometryEquiv.
Instances For
@[simp]
theorem
AffineIsometryEquiv.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}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[SeminormedAddCommGroup V₃]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[NormedSpace 𝕜 V₃]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[PseudoMetricSpace P₃]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
[NormedAddTorsor V₃ P₃]
(e₁ : P ≃ᵃⁱ[𝕜] P₂)
(e₂ : P₂ ≃ᵃⁱ[𝕜] P₃)
:
↑(AffineIsometryEquiv.trans e₁ e₂) = ↑e₂ ∘ ↑e₁
@[simp]
theorem
AffineIsometryEquiv.trans_refl
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
AffineIsometryEquiv.trans e (AffineIsometryEquiv.refl 𝕜 P₂) = e
@[simp]
theorem
AffineIsometryEquiv.refl_trans
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
@[simp]
theorem
AffineIsometryEquiv.self_trans_symm
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
@[simp]
theorem
AffineIsometryEquiv.symm_trans_self
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
@[simp]
theorem
AffineIsometryEquiv.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}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[SeminormedAddCommGroup V₃]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[NormedSpace 𝕜 V₃]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[PseudoMetricSpace P₃]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
[NormedAddTorsor V₃ P₃]
(e₁ : P ≃ᵃⁱ[𝕜] P₂)
(e₂ : P₂ ≃ᵃⁱ[𝕜] P₃)
:
↑(AffineIsometryEquiv.symm (AffineIsometryEquiv.trans e₁ e₂)) = ↑(AffineIsometryEquiv.symm e₁) ∘ ↑(AffineIsometryEquiv.symm e₂)
theorem
AffineIsometryEquiv.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}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[SeminormedAddCommGroup V₃]
[SeminormedAddCommGroup V₄]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[NormedSpace 𝕜 V₃]
[NormedSpace 𝕜 V₄]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[PseudoMetricSpace P₃]
[PseudoMetricSpace P₄]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
[NormedAddTorsor V₃ P₃]
[NormedAddTorsor V₄ P₄]
(ePP₂ : P ≃ᵃⁱ[𝕜] P₂)
(eP₂G : P₂ ≃ᵃⁱ[𝕜] P₃)
(eGG' : P₃ ≃ᵃⁱ[𝕜] P₄)
:
AffineIsometryEquiv.trans ePP₂ (AffineIsometryEquiv.trans eP₂G eGG') = AffineIsometryEquiv.trans (AffineIsometryEquiv.trans ePP₂ eP₂G) eGG'
instance
AffineIsometryEquiv.instGroupAffineIsometryEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
The group of affine isometries of a NormedAddTorsor, P.
@[simp]
theorem
AffineIsometryEquiv.coe_one
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[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_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(e : P ≃ᵃⁱ[𝕜] P)
(e' : P ≃ᵃⁱ[𝕜] P)
:
@[simp]
theorem
AffineIsometryEquiv.coe_inv
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(e : P ≃ᵃⁱ[𝕜] P)
:
↑e⁻¹ = ↑(AffineIsometryEquiv.symm e)
@[simp]
theorem
AffineIsometryEquiv.map_vadd
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(p : P)
(v : V)
:
↑e (v +ᵥ p) = ↑(AffineIsometryEquiv.linearIsometryEquiv e) v +ᵥ ↑e p
@[simp]
theorem
AffineIsometryEquiv.map_vsub
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(p1 : P)
(p2 : P)
:
↑(AffineIsometryEquiv.linearIsometryEquiv e) (p1 -ᵥ p2) = ↑e p1 -ᵥ ↑e p2
@[simp]
theorem
AffineIsometryEquiv.dist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(x : P)
(y : P)
:
@[simp]
theorem
AffineIsometryEquiv.edist_map
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
(x : P)
(y : P)
:
theorem
AffineIsometryEquiv.bijective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
theorem
AffineIsometryEquiv.injective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
theorem
AffineIsometryEquiv.surjective
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
theorem
AffineIsometryEquiv.map_eq_iff
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
{x : P}
{y : P}
:
theorem
AffineIsometryEquiv.map_ne
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
{x : P}
{y : P}
(h : x ≠ y)
:
↑e x ≠ ↑e y
theorem
AffineIsometryEquiv.lipschitz
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
:
LipschitzWith 1 ↑e
theorem
AffineIsometryEquiv.antilipschitz
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
{α : Type u_12}
[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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
(e : P ≃ᵃⁱ[𝕜] P₂)
{α : Type u_12}
[TopologicalSpace α]
{f : α → P}
:
Continuous (↑e ∘ f) ↔ Continuous f
def
AffineIsometryEquiv.vaddConst
(𝕜 : Type u_1)
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
:
The map v ↦ v +ᵥ p as an affine isometric equivalence between V and P.
Instances For
@[simp]
theorem
AffineIsometryEquiv.coe_vaddConst
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
:
↑(AffineIsometryEquiv.vaddConst 𝕜 p) = fun v => v +ᵥ p
@[simp]
theorem
AffineIsometryEquiv.coe_vaddConst'
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
:
↑(AffineEquiv.vaddConst 𝕜 p) = fun v => v +ᵥ p
@[simp]
theorem
AffineIsometryEquiv.coe_vaddConst_symm
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
:
↑(AffineIsometryEquiv.symm (AffineIsometryEquiv.vaddConst 𝕜 p)) = fun p' => p' -ᵥ p
@[simp]
theorem
AffineIsometryEquiv.vaddConst_toAffineEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
:
(AffineIsometryEquiv.vaddConst 𝕜 p).toAffineEquiv = AffineEquiv.vaddConst 𝕜 p
def
AffineIsometryEquiv.constVSub
(𝕜 : Type u_1)
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
:
p' ↦ p -ᵥ p' as an affine isometric equivalence.
Instances For
@[simp]
theorem
AffineIsometryEquiv.coe_constVSub
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
:
↑(AffineIsometryEquiv.constVSub 𝕜 p) = (fun x x_1 => x -ᵥ x_1) p
@[simp]
theorem
AffineIsometryEquiv.symm_constVSub
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
:
def
AffineIsometryEquiv.constVAdd
(𝕜 : Type u_1)
{V : Type u_2}
(P : Type u_8)
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(v : V)
:
Translation by v (that is, the map p ↦ v +ᵥ p) as an affine isometric automorphism of P.
Instances For
@[simp]
theorem
AffineIsometryEquiv.coe_constVAdd
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(v : V)
:
↑(AffineIsometryEquiv.constVAdd 𝕜 P v) = (fun x x_1 => x +ᵥ x_1) v
@[simp]
theorem
AffineIsometryEquiv.constVAdd_zero
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
:
theorem
AffineIsometryEquiv.vadd_vsub
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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)
:
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
AffineIsometryEquiv.pointReflection
(𝕜 : Type u_1)
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
:
Point reflection in x as an affine isometric automorphism.
Instances For
theorem
AffineIsometryEquiv.pointReflection_apply
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
(y : P)
:
↑(AffineIsometryEquiv.pointReflection 𝕜 x) y = x -ᵥ y +ᵥ x
@[simp]
theorem
AffineIsometryEquiv.pointReflection_toAffineEquiv
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
:
(AffineIsometryEquiv.pointReflection 𝕜 x).toAffineEquiv = AffineEquiv.pointReflection 𝕜 x
@[simp]
theorem
AffineIsometryEquiv.pointReflection_self
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
:
↑(AffineIsometryEquiv.pointReflection 𝕜 x) x = x
theorem
AffineIsometryEquiv.pointReflection_involutive
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
:
@[simp]
theorem
AffineIsometryEquiv.pointReflection_symm
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
:
@[simp]
theorem
AffineIsometryEquiv.dist_pointReflection_fixed
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
(y : P)
:
dist (↑(AffineIsometryEquiv.pointReflection 𝕜 x) y) x = dist y x
theorem
AffineIsometryEquiv.dist_pointReflection_self'
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
(y : P)
:
theorem
AffineIsometryEquiv.dist_pointReflection_self
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(x : P)
(y : P)
:
theorem
AffineIsometryEquiv.pointReflection_fixed_iff
{𝕜 : Type u_1}
{V : Type u_2}
{P : Type u_8}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[NormedSpace 𝕜 V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
[Invertible 2]
{x : P}
{y : P}
:
↑(AffineIsometryEquiv.pointReflection 𝕜 x) y = y ↔ y = x
theorem
AffineIsometryEquiv.dist_pointReflection_self_real
{V : Type u_2}
{P : Type u_8}
[SeminormedAddCommGroup V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
[NormedSpace ℝ V]
(x : P)
(y : P)
:
@[simp]
theorem
AffineIsometryEquiv.pointReflection_midpoint_left
{V : Type u_2}
{P : Type u_8}
[SeminormedAddCommGroup V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
[NormedSpace ℝ V]
(x : P)
(y : P)
:
↑(AffineIsometryEquiv.pointReflection ℝ (midpoint ℝ x y)) x = y
@[simp]
theorem
AffineIsometryEquiv.pointReflection_midpoint_right
{V : Type u_2}
{P : Type u_8}
[SeminormedAddCommGroup V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
[NormedSpace ℝ V]
(x : P)
(y : P)
:
↑(AffineIsometryEquiv.pointReflection ℝ (midpoint ℝ x y)) y = x
theorem
AffineMap.continuous_linear_iff
{𝕜 : Type u_1}
{V : Type u_2}
{V₂ : Type u_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V 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_4}
{P : Type u_8}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V]
[NormedSpace 𝕜 V₂]
[PseudoMetricSpace P]
[PseudoMetricSpace P₂]
[NormedAddTorsor V P]
[NormedAddTorsor V₂ P₂]
{f : P →ᵃ[𝕜] P₂}
:
If f is an affine map, then its linear part is an open map iff f is an open map.
@[simp]
theorem
AffineSubspace.equivMapOfInjective_toFun
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : Function.Injective ↑φ)
:
∀ (a : ↑↑E), ↑(AffineSubspace.equivMapOfInjective E φ hφ) a = Equiv.toFun (Equiv.Set.image (↑φ) (↑E) hφ) a
@[simp]
theorem
AffineSubspace.linear_equivMapOfInjective
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : Function.Injective ↑φ)
:
(AffineSubspace.equivMapOfInjective E φ hφ).linear = LinearEquiv.trans
(Submodule.equivMapOfInjective φ.linear (_ : Function.Injective ↑φ.linear) (AffineSubspace.direction E))
(LinearEquiv.ofEq (Submodule.map φ.linear (AffineSubspace.direction E))
(AffineSubspace.direction (AffineSubspace.map φ E))
(_ : Submodule.map φ.linear (AffineSubspace.direction E) = AffineSubspace.direction (AffineSubspace.map φ E)))
@[simp]
theorem
AffineSubspace.equivMapOfInjective_symm_apply
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : Function.Injective ↑φ)
:
∀ (a : ↑(↑φ '' ↑E)),
↑(AffineEquiv.symm (AffineSubspace.equivMapOfInjective E φ hφ)) a = Equiv.invFun (Equiv.Set.image (↑φ) (↑E) hφ) a
@[simp]
theorem
AffineSubspace.equivMapOfInjective_apply
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : Function.Injective ↑φ)
:
∀ (a : ↑↑E), ↑(AffineSubspace.equivMapOfInjective E φ hφ) a = Equiv.toFun (Equiv.Set.image (↑φ) (↑E) hφ) a
@[simp]
theorem
AffineSubspace.equivMapOfInjective_invFun
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : Function.Injective ↑φ)
:
∀ (a : ↑(↑φ '' ↑E)),
Equiv.invFun (AffineSubspace.equivMapOfInjective E φ hφ).toEquiv a = Equiv.invFun (Equiv.Set.image (↑φ) (↑E) hφ) a
noncomputable def
AffineSubspace.equivMapOfInjective
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
(φ : P₁ →ᵃ[𝕜] P₂)
(hφ : Function.Injective ↑φ)
:
{ x // x ∈ E } ≃ᵃ[𝕜] { x // x ∈ AffineSubspace.map φ E }
An affine subspace is isomorphic to its image under an injective affine map.
This is the affine version of Submodule.equivMapOfInjective.
Instances For
noncomputable def
AffineSubspace.isometryEquivMap
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(φ : P₁ →ᵃⁱ[𝕜] P₂)
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
:
{ x // x ∈ E } ≃ᵃⁱ[𝕜] { x // x ∈ AffineSubspace.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.
Instances For
@[simp]
theorem
AffineSubspace.isometryEquivMap.apply_symm_apply
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
{E : AffineSubspace 𝕜 P₁}
[Nonempty { x // x ∈ E }]
{φ : P₁ →ᵃⁱ[𝕜] P₂}
(x : { x // x ∈ AffineSubspace.map φ.toAffineMap E })
:
↑φ ↑(↑(AffineIsometryEquiv.symm (AffineSubspace.isometryEquivMap φ E)) x) = ↑x
@[simp]
theorem
AffineSubspace.isometryEquivMap.coe_apply
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(φ : P₁ →ᵃⁱ[𝕜] P₂)
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
(g : { x // x ∈ E })
:
↑(↑(AffineSubspace.isometryEquivMap φ E) g) = ↑φ ↑g
@[simp]
theorem
AffineSubspace.isometryEquivMap.toAffineMap_eq
{𝕜 : Type u_1}
{V₁ : Type u_3}
{V₂ : Type u_4}
{P₁ : Type u_7}
{P₂ : Type u_9}
[NormedField 𝕜]
[SeminormedAddCommGroup V₁]
[SeminormedAddCommGroup V₂]
[NormedSpace 𝕜 V₁]
[NormedSpace 𝕜 V₂]
[MetricSpace P₁]
[PseudoMetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
(φ : P₁ →ᵃⁱ[𝕜] P₂)
(E : AffineSubspace 𝕜 P₁)
[Nonempty { x // x ∈ E }]
:
↑(AffineSubspace.isometryEquivMap φ E).toAffineEquiv = ↑(AffineSubspace.equivMapOfInjective E φ.toAffineMap (_ : Function.Injective ↑φ))