Mathlib.Analysis.Normed.Affine.Isometry

AffineIsometry structure

extends P →ᵃ[𝕜] P₂

Full source

/-- A `𝕜`-affine isometric embedding of one normed add-torsor over a normed `𝕜`-space into
another, denoted as `f : P →ᵃⁱ[𝕜] P₂`. -/
structure AffineIsometry extends P →ᵃ[𝕜] P₂ where
  norm_map : ∀ x : V, ‖linear x‖ = ‖x‖

Affine isometric embedding

Informal description

An affine isometric embedding from a normed affine space $ P $ to another normed affine space $ P₂ $ over a normed $ \mathbb{K} $-space, denoted $ f: P \to^{a\mathbb{K}} P₂ $, is a structure that extends an affine map while preserving distances between points.

term_→ᵃⁱ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 -- `→ᵃᵢ` would be more consistent with the linear isometry notation, but it is uglier
P " →ᵃⁱ[" 𝕜:25 "] " P₂:0 => AffineIsometry 𝕜 P P₂

Affine isometric embedding notation

Informal description

The notation $ P \to^{ai}[\mathbb{K}] P_2 $ represents an affine isometric embedding from the normed affine space $ P $ to the normed affine space $ P_2 $ over the normed $\mathbb{K}$-space.

AffineIsometry.linearIsometry definition

: V →ₗᵢ[𝕜] V₂

Full source

/-- The underlying linear map of an affine isometry is in fact a linear isometry. -/
protected def linearIsometry : V →ₗᵢ[𝕜] V₂ :=
  { f.linear with norm_map' := f.norm_map }

Linear isometry underlying an affine isometry

Informal description

The underlying linear map of an affine isometry $ f : P \to^{a\mathbb{K}} P₂ $ is a linear isometry $ V \to^{𝕜} V₂ $ between the corresponding normed vector spaces, preserving the norm: $ \|f.linearIsometry(v)\| = \|v\| $ for all $ v \in V $.

AffineIsometry.linear_eq_linearIsometry theorem

: f.linear = f.linearIsometry.toLinearMap

Full source

@[simp]
theorem linear_eq_linearIsometry : f.linear = f.linearIsometry.toLinearMap := by
  ext
  rfl

Equality of Linear Part and Linear Isometry in Affine Isometric Embedding

Informal description

For an affine isometric embedding $f : P \to^{a\mathbb{K}} P₂$, the linear part of $f$ is equal to the underlying linear map of its associated linear isometry.

AffineIsometry.instFunLike instance

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

Full source

instance : FunLike (P →ᵃⁱ[𝕜] P₂) P P₂ where
  coe f := f.toFun
  coe_injective' f g := by cases f; cases g; simp

Function-Like Structure of Affine Isometric Embeddings

Informal description

For any affine isometric embedding $f : P \to^{a\mathbb{K}} P₂$ between normed affine spaces over a normed $\mathbb{K}$-space, the type of such embeddings $(P \to^{a\mathbb{K}} P₂)$ has a function-like structure, meaning it can be coerced to a function from $P$ to $P₂$ in an injective way.

AffineIsometry.coe_toAffineMap theorem

: ⇑f.toAffineMap = f

Full source

@[simp]
theorem coe_toAffineMap : ⇑f.toAffineMap = f := by
  rfl

Underlying Affine Map of Affine Isometry is the Isometry Itself

Informal description

For an affine isometric embedding $f : P \to^{a\mathbb{K}} P₂$, the underlying affine map of $f$ is equal to $f$ when viewed as a function.

AffineIsometry.toAffineMap_injective theorem

: Injective (toAffineMap : (P →ᵃⁱ[𝕜] P₂) → P →ᵃ[𝕜] P₂)

Full source

theorem toAffineMap_injective : Injective (toAffineMap : (P →ᵃⁱ[𝕜] P₂) → P →ᵃ[𝕜] P₂) := by
  rintro ⟨f, _⟩ ⟨g, _⟩ rfl
  rfl

Injectivity of the Underlying Affine Map of an Affine Isometry

Informal description

The map that takes an affine isometric embedding $f : P \to^{a\mathbb{K}} P₂$ to its underlying affine map is injective. In other words, if two affine isometric embeddings have the same underlying affine map, then they must be equal.

AffineIsometry.coeFn_injective theorem

: @Injective (P →ᵃⁱ[𝕜] P₂) (P → P₂) (↑)

Full source

theorem coeFn_injective : @Injective (P →ᵃⁱ[𝕜] P₂) (P → P₂) (↑) :=
  AffineMap.coeFn_injective.comp toAffineMap_injective

Injectivity of the Underlying Function of an Affine Isometry

Informal description

The canonical function that maps an affine isometric embedding $f \colon P \to^{a\mathbb{K}} P₂$ to its underlying function $f \colon P \to P₂$ is injective. In other words, if two affine isometric embeddings have the same underlying function, then they must be equal.

AffineIsometry.ext theorem

{f g : P →ᵃⁱ[𝕜] P₂} (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext {f g : P →ᵃⁱ[𝕜] P₂} (h : ∀ x, f x = g x) : f = g :=
  coeFn_injective <| funext h

Extensionality of Affine Isometric Embeddings

Informal description

For any two affine isometric embeddings $ f, g \colon P \to^{a\mathbb{K}} P₂ $, if $ f(x) = g(x) $ for all $ x \in P $, then $ f = g $.

LinearIsometry.toAffineIsometry definition

: V →ᵃⁱ[𝕜] V₂

Full source

/-- Reinterpret a linear isometry as an affine isometry. -/
def toAffineIsometry : V →ᵃⁱ[𝕜] V₂ :=
  { f.toLinearMap.toAffineMap with norm_map := f.norm_map }

Affine isometry from linear isometry

Informal description

The function converts a linear isometry $ f: V \to V₂ $ into an affine isometry $ V \to^{a𝕜} V₂ $ by extending the linear map to an affine map while preserving the norm. That is, for any $ x \in V $, the norm of $ f(x) $ equals the norm of $ x $.

LinearIsometry.coe_toAffineIsometry theorem

: ⇑(f.toAffineIsometry : V →ᵃⁱ[𝕜] V₂) = f

Full source

@[simp]
theorem coe_toAffineIsometry : ⇑(f.toAffineIsometry : V →ᵃⁱ[𝕜] V₂) = f :=
  rfl

Underlying Function of Affine Isometry from Linear Isometry Equals Original Function

Informal description

For a linear isometry $f : V \to V₂$ between normed vector spaces over $\mathbb{K}$, the underlying function of the corresponding affine isometry $f.toAffineIsometry : V \to^{a\mathbb{K}} V₂$ is equal to $f$ itself.

LinearIsometry.toAffineIsometry_linearIsometry theorem

: f.toAffineIsometry.linearIsometry = f

Full source

@[simp]
theorem toAffineIsometry_linearIsometry : f.toAffineIsometry.linearIsometry = f := by
  ext
  rfl

Underlying Linear Isometry of Affine Isometry from Linear Isometry Equals Original

Informal description

For a linear isometry $f \colon V \to V₂$ between normed vector spaces over $\mathbb{K}$, the underlying linear isometry of the corresponding affine isometry $f.toAffineIsometry$ is equal to $f$ itself.

LinearIsometry.toAffineIsometry_toAffineMap theorem

: f.toAffineIsometry.toAffineMap = f.toLinearMap.toAffineMap

Full source

@[simp]
theorem toAffineIsometry_toAffineMap : f.toAffineIsometry.toAffineMap = f.toLinearMap.toAffineMap :=
  rfl

Affine Map Correspondence for Linear Isometry to Affine Isometry

Informal description

For a linear isometry $f : V \to V₂$, the affine map associated with its corresponding affine isometry is equal to the affine map obtained from the linear map underlying $f$.

AffineIsometry.map_vadd theorem

(p : P) (v : V) : f (v +ᵥ p) = f.linearIsometry v +ᵥ f p

Full source

@[simp]
theorem map_vadd (p : P) (v : V) : f (v +ᵥ p) = f.linearIsometry v +ᵥ f p :=
  f.toAffineMap.map_vadd p v

Affine Isometry Preserves Vector Addition

Informal description

For an affine isometry $f \colon P \to^{a\mathbb{K}} P₂$, a point $p \in P$, and a vector $v \in V$, the action of $f$ on the sum $v + p$ is given by $f(v + p) = f.linearIsometry(v) + f(p)$, where $f.linearIsometry$ is the underlying linear isometry of $f$.

AffineIsometry.map_vsub theorem

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

Full source

@[simp]
theorem map_vsub (p1 p2 : P) : f.linearIsometry (p1 -ᵥ p2) = f p1 -ᵥ f p2 :=
  f.toAffineMap.linearMap_vsub p1 p2

Affine Isometry Preserves Vector Difference

Informal description

For any affine isometry $f \colon P \to P₂$ and any two points $p₁, p₂ \in P$, the linear isometry underlying $f$ applied to the vector difference $p₁ - p₂$ equals the vector difference of the images $f(p₁) - f(p₂)$ in $P₂$.

AffineIsometry.dist_map theorem

(x y : P) : dist (f x) (f y) = dist x y

Full source

@[simp]
theorem dist_map (x y : P) : dist (f x) (f y) = dist x y := by
  rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]

Distance Preservation under Affine Isometry

Informal description

For any affine isometry $f \colon P \to P₂$ and any two points $x, y \in P$, the distance between $f(x)$ and $f(y)$ in $P₂$ is equal to the distance between $x$ and $y$ in $P$, i.e., $\operatorname{dist}(f(x), f(y)) = \operatorname{dist}(x, y)$.

AffineIsometry.nndist_map theorem

(x y : P) : nndist (f x) (f y) = nndist x y

Full source

@[simp]
theorem nndist_map (x y : P) : nndist (f x) (f y) = nndist x y := by simp [nndist_dist]

Non-Negative Distance Preservation under Affine Isometry

Informal description

For any affine isometry $f \colon P \to P₂$ and any two points $x, y \in P$, the non-negative distance between $f(x)$ and $f(y)$ in $P₂$ is equal to the non-negative distance between $x$ and $y$ in $P$, i.e., $\operatorname{nndist}(f(x), f(y)) = \operatorname{nndist}(x, y)$.

AffineIsometry.edist_map theorem

(x y : P) : edist (f x) (f y) = edist x y

Full source

@[simp]
theorem edist_map (x y : P) : edist (f x) (f y) = edist x y := by simp [edist_dist]

Extended Distance Preservation under Affine Isometry

Informal description

For any affine isometry $f \colon P \to P₂$ and any two points $x, y \in P$, the extended distance between $f(x)$ and $f(y)$ in $P₂$ is equal to the extended distance between $x$ and $y$ in $P$, i.e., $\operatorname{edist}(f(x), f(y)) = \operatorname{edist}(x, y)$.

AffineIsometry.isometry theorem

: Isometry f

Full source

protected theorem isometry : Isometry f :=
  f.edist_map

Affine Isometry Preserves Distance

Informal description

An affine isometry $f \colon P \to P₂$ is an isometry, meaning it preserves distances between points in the metric space.

AffineIsometry.injective theorem

: Injective f₁

Full source

protected theorem injective : Injective f₁ :=
  f₁.isometry.injective

Injectivity of Affine Isometries

Informal description

An affine isometry $f_1 \colon P_1 \to P_2$ is injective, meaning that for any two points $x, y \in P_1$, if $f_1(x) = f_1(y)$, then $x = y$.

AffineIsometry.map_eq_iff theorem

{x y : P₁'} : f₁ x = f₁ y ↔ x = y

Full source

@[simp]
theorem map_eq_iff {x y : P₁'} : f₁ x = f₁ y ↔ x = y :=
  f₁.injective.eq_iff

Affine Isometry Preserves Distinctness

Informal description

For any affine isometry $f_1 \colon P_1 \to P_2$ and any two points $x, y \in P_1$, the images $f_1(x)$ and $f_1(y)$ are equal if and only if $x = y$.

AffineIsometry.map_ne theorem

{x y : P₁'} (h : x ≠ y) : f₁ x ≠ f₁ y

Full source

theorem map_ne {x y : P₁'} (h : x ≠ y) : f₁ x ≠ f₁ y :=
  f₁.injective.ne h

Affine Isometry Preserves Distinctness of Points

Informal description

For any affine isometry $f_1 \colon P_1' \to P_2$ and any two distinct points $x, y \in P_1'$ (i.e., $x \neq y$), the images $f_1(x)$ and $f_1(y)$ are distinct.

AffineIsometry.lipschitz theorem

: LipschitzWith 1 f

Full source

protected theorem lipschitz : LipschitzWith 1 f :=
  f.isometry.lipschitz

Affine Isometry is 1-Lipschitz

Informal description

An affine isometry $f \colon P \to P₂$ is Lipschitz continuous with constant $1$, i.e., for any two points $x, y \in P$, the distance between $f(x)$ and $f(y)$ is at most the distance between $x$ and $y$.

AffineIsometry.antilipschitz theorem

: AntilipschitzWith 1 f

Full source

protected theorem antilipschitz : AntilipschitzWith 1 f :=
  f.isometry.antilipschitz

Affine Isometry is Antilipschitz with Constant 1

Informal description

An affine isometry $f \colon P \to P₂$ is antilipschitz with constant $1$, meaning that for any two points $x, y \in P$, the distance between $f(x)$ and $f(y)$ is at least the distance between $x$ and $y$.

AffineIsometry.continuous theorem

: Continuous f

Full source

@[continuity]
protected theorem continuous : Continuous f :=
  f.isometry.continuous

Continuity of Affine Isometries

Informal description

An affine isometry $f \colon P \to P₂$ is continuous.

AffineIsometry.ediam_image theorem

(s : Set P) : EMetric.diam (f '' s) = EMetric.diam s

Full source

theorem ediam_image (s : Set P) : EMetric.diam (f '' s) = EMetric.diam s :=
  f.isometry.ediam_image s

Affine Isometry Preserves Extended Diameter of Subsets

Informal description

For any affine isometry $f \colon P \to P₂$ and any subset $s \subseteq P$, the extended diameter of the image $f(s)$ is equal to the extended diameter of $s$, i.e., $\text{diam}(f(s)) = \text{diam}(s)$.

AffineIsometry.ediam_range theorem

: EMetric.diam (range f) = EMetric.diam (univ : Set P)

Full source

theorem ediam_range : EMetric.diam (range f) = EMetric.diam (univ : Set P) :=
  f.isometry.ediam_range

Extended Diameter Preservation under Affine Isometry

Informal description

For an affine isometry $f \colon P \to P₂$ between normed affine spaces, the extended diameter of the range of $f$ is equal to the extended diameter of the entire space $P$, i.e., $\text{diam}(\text{range}(f)) = \text{diam}(P)$.

AffineIsometry.diam_image theorem

(s : Set P) : Metric.diam (f '' s) = Metric.diam s

Full source

theorem diam_image (s : Set P) : Metric.diam (f '' s) = Metric.diam s :=
  f.isometry.diam_image s

Affine Isometry Preserves Diameter of Subsets

Informal description

For any affine isometry $f \colon P \to P₂$ and any subset $s \subseteq P$, the diameter of the image $f(s)$ is equal to the diameter of $s$.

AffineIsometry.diam_range theorem

: Metric.diam (range f) = Metric.diam (univ : Set P)

Full source

theorem diam_range : Metric.diam (range f) = Metric.diam (univ : Set P) :=
  f.isometry.diam_range

Diameter Preservation under Affine Isometry

Informal description

For an affine isometry $f \colon P \to P₂$ between normed affine spaces, the diameter of the range of $f$ is equal to the diameter of the entire space $P$, i.e., $\text{diam}(\text{range}(f)) = \text{diam}(P)$.

AffineIsometry.comp_continuous_iff theorem

{α : Type*} [TopologicalSpace α] {g : α → P} : Continuous (f ∘ g) ↔ Continuous g

Full source

@[simp]
theorem comp_continuous_iff {α : Type*} [TopologicalSpace α] {g : α → P} :
    ContinuousContinuous (f ∘ g) ↔ Continuous g :=
  f.isometry.comp_continuous_iff

Continuity of Composition with Affine Isometry

Informal description

Let $P$ and $P₂$ be normed affine spaces over a normed $\mathbb{K}$-space, and let $f \colon P \to P₂$ be an affine isometry. For any topological space $\alpha$ and function $g \colon \alpha \to P$, the composition $f \circ g$ is continuous if and only if $g$ is continuous.

AffineIsometry.id definition

: P →ᵃⁱ[𝕜] P

Full source

/-- The identity affine isometry. -/
def id : P →ᵃⁱ[𝕜] P :=
  ⟨AffineMap.id 𝕜 P, fun _ => rfl⟩

Identity affine isometry

Informal description

The identity affine isometry from a normed affine space $ P $ to itself, denoted $ \text{id}: P \to^{a\mathbb{K}} P $, is the affine isometric embedding that maps every point $ x \in P $ to itself and preserves distances.

AffineIsometry.coe_id theorem

: ⇑(id : P →ᵃⁱ[𝕜] P) = _root_.id

Full source

@[simp, norm_cast]
theorem coe_id : ⇑(id : P →ᵃⁱ[𝕜] P) = _root_.id :=
  rfl

Identity Affine Isometry as Identity Function

Informal description

The underlying function of the identity affine isometry from a normed affine space $P$ to itself is equal to the identity function on $P$.

AffineIsometry.id_apply theorem

(x : P) : (AffineIsometry.id : P →ᵃⁱ[𝕜] P) x = x

Full source

@[simp]
theorem id_apply (x : P) : (AffineIsometry.id : P →ᵃⁱ[𝕜] P) x = x :=
  rfl

Identity Affine Isometry Evaluation at Point $x$

Informal description

For any point $x$ in the normed affine space $P$, the identity affine isometry $\text{id} : P \to^{a\mathbb{K}} P$ satisfies $\text{id}(x) = x$.

AffineIsometry.id_toAffineMap theorem

: (id.toAffineMap : P →ᵃ[𝕜] P) = AffineMap.id 𝕜 P

Full source

@[simp]
theorem id_toAffineMap : (id.toAffineMap : P →ᵃ[𝕜] P) = AffineMap.id 𝕜 P :=
  rfl

Identity Affine Isometry as Identity Affine Map

Informal description

The underlying affine map of the identity affine isometry from a normed affine space $P$ to itself is equal to the identity affine map on $P$ over the field $\mathbb{K}$.

AffineIsometry.instInhabited instance

: Inhabited (P →ᵃⁱ[𝕜] P)

Full source

instance : Inhabited (P →ᵃⁱ[𝕜] P) :=
  ⟨id⟩

Inhabited Type of Affine Isometric Self-Embeddings

Informal description

For any normed affine space $P$ over a normed $\mathbb{K}$-space, the type of affine isometric embeddings from $P$ to itself is inhabited, with the identity affine isometry as a canonical element.

AffineIsometry.comp definition

(g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) : P →ᵃⁱ[𝕜] P₃

Full source

/-- Composition of affine isometries. -/
def comp (g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) : P →ᵃⁱ[𝕜] P₃ :=
  ⟨g.toAffineMap.comp f.toAffineMap, fun _ => (g.norm_map _).trans (f.norm_map _)⟩

Composition of affine isometric embeddings

Informal description

The composition of two affine isometric embeddings $ g : P₂ \to^{a\mathbb{K}} P₃ $ and $ f : P \to^{a\mathbb{K}} P₂ $ is an affine isometric embedding $ g \circ f : P \to^{a\mathbb{K}} P₃ $ that preserves distances between points.

AffineIsometry.coe_comp theorem

(g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) : ⇑(g.comp f) = g ∘ f

Full source

@[simp]
theorem coe_comp (g : P₂ →ᵃⁱ[𝕜] P₃) (f : P →ᵃⁱ[𝕜] P₂) : ⇑(g.comp f) = g ∘ f :=
  rfl

Composition of Affine Isometric Embeddings Preserves Function Application

Informal description

For any affine isometric embeddings $g \colon P_2 \to^{a\mathbb{K}} P_3$ and $f \colon P \to^{a\mathbb{K}} P_2$, the underlying function of their composition $g \circ f$ is equal to the composition of their underlying functions, i.e., $(g \circ f)(x) = g(f(x))$ for all $x \in P$.

AffineIsometry.id_comp theorem

: (id : P₂ →ᵃⁱ[𝕜] P₂).comp f = f

Full source

@[simp]
theorem id_comp : (id : P₂ →ᵃⁱ[𝕜] P₂).comp f = f :=
  ext fun _ => rfl

Left Identity Property of Affine Isometric Embedding Composition

Informal description

For any affine isometric embedding $f \colon P \to^{a\mathbb{K}} P₂$, the composition of the identity affine isometry on $P₂$ with $f$ is equal to $f$ itself, i.e., $\text{id} \circ f = f$.

AffineIsometry.comp_id theorem

: f.comp id = f

Full source

@[simp]
theorem comp_id : f.comp id = f :=
  ext fun _ => rfl

Right Identity Property of Affine Isometric Embedding Composition

Informal description

For any affine isometric embedding $f \colon P \to^{a\mathbb{K}} P₂$, the composition of $f$ with the identity affine isometry on $P₂$ is equal to $f$ itself, i.e., $f \circ \text{id} = f$.

AffineIsometry.comp_assoc theorem

 (f : P₃ →ᵃⁱ[𝕜] P₄) (g : P₂ →ᵃⁱ[𝕜] P₃) (h : P →ᵃⁱ[𝕜] P₂) : (f.comp g).comp h = f.comp (g.comp h)

Full source

theorem comp_assoc (f : P₃ →ᵃⁱ[𝕜] P₄) (g : P₂ →ᵃⁱ[𝕜] P₃) (h : P →ᵃⁱ[𝕜] P₂) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition of Affine Isometric Embeddings

Informal description

For any affine isometric embeddings $f \colon P₃ \to^{a\mathbb{K}} P₄$, $g \colon P₂ \to^{a\mathbb{K}} P₃$, and $h \colon P \to^{a\mathbb{K}} P₂$, the composition of affine isometric embeddings is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.

AffineIsometry.instMonoid instance

: Monoid (P →ᵃⁱ[𝕜] P)

Full source

instance : Monoid (P →ᵃⁱ[𝕜] P) where
  one := id
  mul := comp
  mul_assoc := comp_assoc
  one_mul := id_comp
  mul_one := comp_id

Monoid Structure on Affine Isometries

Informal description

The set of affine isometries from a normed affine space $ P $ to itself over a normed $ \mathbb{K} $-space forms a monoid under composition, with the identity affine isometry as the neutral element.

AffineIsometry.coe_one theorem

: ⇑(1 : P →ᵃⁱ[𝕜] P) = _root_.id

Full source

@[simp]
theorem coe_one : ⇑(1 : P →ᵃⁱ[𝕜] P) = _root_.id :=
  rfl

Identity Affine Isometry Yields Identity Function

Informal description

The underlying function of the identity affine isometry $1 \colon P \to^{a\mathbb{K}} P$ is equal to the identity function $\mathrm{id} \colon P \to P$.

AffineIsometry.coe_mul theorem

(f g : P →ᵃⁱ[𝕜] P) : ⇑(f * g) = f ∘ g

Full source

@[simp]
theorem coe_mul (f g : P →ᵃⁱ[𝕜] P) : ⇑(f * g) = f ∘ g :=
  rfl

Composition of Affine Isometries as Function Composition

Informal description

For any two affine isometries $f, g : P \to^{a\mathbb{K}} P$ on a normed affine space $P$ over a normed field $\mathbb{K}$, the underlying function of their composition $f * g$ is equal to the function composition $f \circ g$.

AffineSubspace.subtypeₐᵢ definition

(s : AffineSubspace 𝕜 P) [Nonempty s] : s →ᵃⁱ[𝕜] P

Full source

/-- `AffineSubspace.subtype` as an `AffineIsometry`. -/
def subtypeₐᵢ (s : AffineSubspace 𝕜 P) [Nonempty s] : s →ᵃⁱ[𝕜] P :=
  { s.subtype with norm_map := s.direction.subtypeₗᵢ.norm_map }

Affine isometric embedding of an affine subspace

Informal description

For a nonempty affine subspace $ s $ of a normed affine space $ P $ over a normed field $ \mathbb{K} $, the canonical inclusion map $ s \hookrightarrow P $ is an affine isometric embedding. This means it preserves both the affine structure and the distances between points in $ s $.

AffineSubspace.subtypeₐᵢ_linear theorem

(s : AffineSubspace 𝕜 P) [Nonempty s] : s.subtypeₐᵢ.linear = s.direction.subtype

Full source

theorem subtypeₐᵢ_linear (s : AffineSubspace 𝕜 P) [Nonempty s] :
    s.subtypeₐᵢ.linear = s.direction.subtype :=
  rfl

Linear Part of Affine Isometric Subspace Embedding Equals Direction Subspace Embedding

Informal description

For any nonempty affine subspace $s$ of a normed affine space $P$ over a normed field $\mathbb{K}$, the linear part of the affine isometric embedding $\text{subtype}_{\text{ai}} : s \hookrightarrow P$ is equal to the canonical linear embedding of the direction subspace $s.\text{direction}$ into the underlying vector space of $P$.

AffineSubspace.subtypeₐᵢ_linearIsometry theorem

(s : AffineSubspace 𝕜 P) [Nonempty s] : s.subtypeₐᵢ.linearIsometry = s.direction.subtypeₗᵢ

Full source

@[simp]
theorem subtypeₐᵢ_linearIsometry (s : AffineSubspace 𝕜 P) [Nonempty s] :
    s.subtypeₐᵢ.linearIsometry = s.direction.subtypeₗᵢ :=
  rfl

Equality of Linear Isometries in Affine Subspace Embedding

Informal description

For any nonempty affine subspace $s$ of a normed affine space $P$ over a normed field $\mathbb{K}$, the linear isometry underlying the canonical affine isometric embedding $s \hookrightarrow P$ is equal to the canonical linear isometric embedding of the direction subspace $s.\text{direction}$ into the underlying vector space of $P$.

AffineSubspace.coe_subtypeₐᵢ theorem

(s : AffineSubspace 𝕜 P) [Nonempty s] : ⇑s.subtypeₐᵢ = s.subtype

Full source

@[simp]
theorem coe_subtypeₐᵢ (s : AffineSubspace 𝕜 P) [Nonempty s] : ⇑s.subtypeₐᵢ = s.subtype :=
  rfl

Inclusion of Affine Subspace as Affine Isometric Embedding

Informal description

For any nonempty affine subspace $s$ of a normed affine space $P$ over a normed field $\mathbb{K}$, the canonical inclusion map $\text{subtype}_{\text{ai}} : s \hookrightarrow P$ is equal to the underlying affine subspace inclusion map $\text{subtype}$.

AffineSubspace.subtypeₐᵢ_toAffineMap theorem

(s : AffineSubspace 𝕜 P) [Nonempty s] : s.subtypeₐᵢ.toAffineMap = s.subtype

Full source

@[simp]
theorem subtypeₐᵢ_toAffineMap (s : AffineSubspace 𝕜 P) [Nonempty s] :
    s.subtypeₐᵢ.toAffineMap = s.subtype :=
  rfl

Affine isometric embedding coincides with subspace inclusion as affine maps

Informal description

For any nonempty affine subspace $s$ of a normed affine space $P$ over a normed field $\mathbb{K}$, the underlying affine map of the canonical affine isometric embedding $s \hookrightarrow P$ is equal to the affine subspace inclusion map $s \hookrightarrow P$.

AffineIsometryEquiv structure

extends P ≃ᵃ[𝕜] P₂

Full source

/-- An affine isometric equivalence between two normed vector spaces,
denoted `f : P ≃ᵃⁱ[𝕜] P₂`. -/
structure AffineIsometryEquiv extends P ≃ᵃ[𝕜] P₂ where
  norm_map : ∀ x, ‖linear x‖ = ‖x‖

Affine Isometric Equivalence

Informal description

An affine isometric equivalence between two normed vector spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, denoted by $f : P \simeq^{ai}[\mathbb{K}] P₂$. This structure extends the notion of an affine equivalence ($P \simeq^a[\mathbb{K}] P₂$) by additionally requiring that the map preserves distances, i.e., it is an isometry.

term_≃ᵃⁱ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] notation:25 P " ≃ᵃⁱ[" 𝕜:25 "] " P₂:0 => AffineIsometryEquiv 𝕜 P P₂

Affine isometric equivalence notation

Informal description

The notation $ P \simeq^{ai}[\mathbb{K}] P_2 $ represents an affine isometric equivalence between the normed affine spaces $ P $ and $ P_2 $ over the normed $ \mathbb{K} $-space. This is a bijective affine map that preserves distances.

AffineIsometryEquiv.linearIsometryEquiv definition

: V ≃ₗᵢ[𝕜] V₂

Full source

/-- The underlying linear equiv of an affine isometry equiv is in fact a linear isometry equiv. -/
protected def linearIsometryEquiv : V ≃ₗᵢ[𝕜] V₂ :=
  { e.linear with norm_map' := e.norm_map }

Linear isometric equivalence underlying an affine isometric equivalence

Informal description

The underlying linear map of an affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ between normed vector spaces $P$ and $P₂$ over a normed field $\mathbb{K}$ is in fact a linear isometric equivalence $V \simeq^{li}[\mathbb{K}] V₂$ between the corresponding normed vector spaces $V$ and $V₂$.

AffineIsometryEquiv.linear_eq_linear_isometry theorem

: e.linear = e.linearIsometryEquiv.toLinearEquiv

Full source

@[simp]
theorem linear_eq_linear_isometry : e.linear = e.linearIsometryEquiv.toLinearEquiv := by
  ext
  rfl

Equality of Linear Parts in Affine Isometric Equivalence

Informal description

For an affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ between normed vector spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, the linear part of $e$ is equal to the underlying linear equivalence of the linear isometric equivalence associated with $e$. In other words, $e.\text{linear} = e.\text{linearIsometryEquiv}.\text{toLinearEquiv}$.

AffineIsometryEquiv.instEquivLike instance

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

Full source

instance : EquivLike (P ≃ᵃⁱ[𝕜] P₂) P P₂ where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' f g h _ := by
    cases f
    cases g
    congr
    simpa [DFunLike.coe_injective.eq_iff] using h

Affine Isometric Equivalence as Bijection

Informal description

For any affine isometric equivalence $f : P \simeq^{ai}[\mathbb{K}] P₂$ between normed vector spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, the map $f$ can be viewed as a bijection between $P$ and $P₂$ that preserves distances.

AffineIsometryEquiv.coe_mk theorem

(e : P ≃ᵃ[𝕜] P₂) (he : ∀ x, ‖e.linear x‖ = ‖x‖) : ⇑(mk e he) = e

Full source

@[simp]
theorem coe_mk (e : P ≃ᵃ[𝕜] P₂) (he : ∀ x, ‖e.linear x‖ = ‖x‖) : ⇑(mk e he) = e :=
  rfl

Construction of Affine Isometric Equivalence Preserves Underlying Function

Informal description

Let $e : P \simeq^a[\mathbb{K}] P₂$ be an affine equivalence between normed vector spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, and suppose that for every $x$, the norm of $e.linear(x)$ equals the norm of $x$. Then the underlying function of the affine isometric equivalence constructed from $e$ with this isometry condition coincides with $e$ itself.

AffineIsometryEquiv.coe_toAffineEquiv theorem

(e : P ≃ᵃⁱ[𝕜] P₂) : ⇑e.toAffineEquiv = e

Full source

@[simp]
theorem coe_toAffineEquiv (e : P ≃ᵃⁱ[𝕜] P₂) : ⇑e.toAffineEquiv = e :=
  rfl

Underlying Affine Equivalence of an Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ between normed vector spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, the underlying affine equivalence map $e.toAffineEquiv$ coincides with $e$ itself when viewed as a function.

AffineIsometryEquiv.toAffineEquiv_injective theorem

: Injective (toAffineEquiv : (P ≃ᵃⁱ[𝕜] P₂) → P ≃ᵃ[𝕜] P₂)

Full source

theorem toAffineEquiv_injective : Injective (toAffineEquiv : (P ≃ᵃⁱ[𝕜] P₂) → P ≃ᵃ[𝕜] P₂)
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

Injectivity of the Affine Equivalence Underlying an Affine Isometric Equivalence

Informal description

The function that maps an affine isometric equivalence $f : P \simeq^{ai}[\mathbb{K}] P₂$ to its underlying affine equivalence is injective. In other words, if two affine isometric equivalences have the same underlying affine equivalence, then they must be equal.

AffineIsometryEquiv.ext theorem

{e e' : P ≃ᵃⁱ[𝕜] P₂} (h : ∀ x, e x = e' x) : e = e'

Full source

@[ext]
theorem ext {e e' : P ≃ᵃⁱ[𝕜] P₂} (h : ∀ x, e x = e' x) : e = e' :=
  toAffineEquiv_injective <| AffineEquiv.ext h

Extensionality of Affine Isometric Equivalences

Informal description

For any two affine isometric equivalences $e, e' : P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, if $e(x) = e'(x)$ for all $x \in P$, then $e = e'$.

AffineIsometryEquiv.toAffineIsometry definition

: P →ᵃⁱ[𝕜] P₂

Full source

/-- Reinterpret an `AffineIsometryEquiv` as an `AffineIsometry`. -/
def toAffineIsometry : P →ᵃⁱ[𝕜] P₂ :=
  ⟨e.1.toAffineMap, e.2⟩

Underlying affine isometric embedding of an affine isometric equivalence

Informal description

Given an affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, the function maps $e$ to its underlying affine isometric embedding $P \to^{ai}[\mathbb{K}] P₂$. This embedding consists of the affine map component of $e$ and inherits the isometry property from $e$.

AffineIsometryEquiv.coe_toAffineIsometry theorem

: ⇑e.toAffineIsometry = e

Full source

@[simp]
theorem coe_toAffineIsometry : ⇑e.toAffineIsometry = e :=
  rfl

Underlying Affine Isometric Embedding of an Affine Isometric Equivalence is the Equivalence Itself

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$, the underlying affine isometric embedding of $e$ is equal to $e$ itself when viewed as a function.

AffineIsometryEquiv.mk' definition

 (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p : P₁) (h : ∀ p' : P₁, e p' = e' (p' -ᵥ p) +ᵥ e p) : P₁ ≃ᵃⁱ[𝕜] P₂

Full source

/-- 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`. -/
def mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p : P₁) (h : ∀ p' : P₁, e p' = e' (p' -ᵥ p) +ᵥ e p) :
    P₁ ≃ᵃⁱ[𝕜] P₂ :=
  { AffineEquiv.mk' e e'.toLinearEquiv p h with norm_map := e'.norm_map }

Affine isometric equivalence from point condition

Informal description

Given a map $e \colon P_1 \to P_2$, a linear isometric equivalence $e' \colon V_1 \simeq_{\mathbb{K}} V_2$, and a point $p \in P_1$ such that for any other point $p' \in P_1$ the relation $e(p') = e'(p' - p) + e(p)$ holds, this constructs an affine isometric equivalence between $P_1$ and $P_2$ over the field $\mathbb{K}$.

AffineIsometryEquiv.coe_mk' theorem

(e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) : ⇑(mk' e e' p h) = e

Full source

@[simp]
theorem coe_mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) : ⇑(mk' e e' p h) = e :=
  rfl

Underlying Function of Affine Isometric Equivalence Constructed via Point Condition

Informal description

Given a map $e \colon P_1 \to P_2$, a linear isometric equivalence $e' \colon V_1 \simeq_{\mathbb{K}} V_2$, a point $p \in P_1$, and a proof $h$ that for all $p' \in P_1$, $e(p') = e'(p' - p) + e(p)$, the underlying function of the affine isometric equivalence constructed via `mk'` is equal to $e$.

AffineIsometryEquiv.linearIsometryEquiv_mk' theorem

(e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) : (mk' e e' p h).linearIsometryEquiv = e'

Full source

@[simp]
theorem linearIsometryEquiv_mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) :
    (mk' e e' p h).linearIsometryEquiv = e' := by
  ext
  rfl

Linear Isometric Equivalence Component of Affine Isometric Equivalence Constructed via Point Condition

Informal description

Given a map $e \colon P_1 \to P_2$, a linear isometric equivalence $e' \colon V_1 \simeq_{\mathbb{K}} V_2$, a point $p \in P_1$, and a proof $h$ that for all $p' \in P_1$ the relation $e(p') = e'(p' - p) + e(p)$ holds, the linear isometric equivalence component of the affine isometric equivalence constructed via `mk'` is equal to $e'$.

LinearIsometryEquiv.toAffineIsometryEquiv definition

: V ≃ᵃⁱ[𝕜] V₂

Full source

/-- Reinterpret a linear isometry equiv as an affine isometry equiv. -/
def toAffineIsometryEquiv : V ≃ᵃⁱ[𝕜] V₂ :=
  { e.toLinearEquiv.toAffineEquiv with norm_map := e.norm_map }

Affine isometric equivalence from linear isometric equivalence

Informal description

Given a linear isometric equivalence $e : V \simeq_{li}[\mathbb{K}] V₂$ between two normed vector spaces $V$ and $V₂$ over a normed field $\mathbb{K}$, the function constructs an affine isometric equivalence $e' : V \simeq^{ai}[\mathbb{K}] V₂$ by extending $e$ to an affine equivalence while preserving the norm. Specifically, the underlying map of $e'$ is the same as $e$, and the linear part of $e'$ is $e$ itself.

LinearIsometryEquiv.coe_toAffineIsometryEquiv theorem

: ⇑(e.toAffineIsometryEquiv : V ≃ᵃⁱ[𝕜] V₂) = e

Full source

@[simp]
theorem coe_toAffineIsometryEquiv : ⇑(e.toAffineIsometryEquiv : V ≃ᵃⁱ[𝕜] V₂) = e := by
  rfl

Underlying Function of Affine Isometric Equivalence from Linear Isometric Equivalence Equals Original Function

Informal description

For any linear isometric equivalence $e : V \simeq_{li}[\mathbb{K}] V₂$ between normed vector spaces $V$ and $V₂$ over a normed field $\mathbb{K}$, the underlying function of the affine isometric equivalence $e' : V \simeq^{ai}[\mathbb{K}] V₂$ obtained from $e$ is equal to $e$ itself. In other words, $\text{fun}(e') = e$.

LinearIsometryEquiv.toAffineIsometryEquiv_linearIsometryEquiv theorem

: e.toAffineIsometryEquiv.linearIsometryEquiv = e

Full source

@[simp]
theorem toAffineIsometryEquiv_linearIsometryEquiv :
    e.toAffineIsometryEquiv.linearIsometryEquiv = e := by
  ext
  rfl

Underlying Linear Isometric Equivalence of Affine Isometric Equivalence from Linear Isometric Equivalence

Informal description

For any linear isometric equivalence $e : V \simeq_{li}[\mathbb{K}] V₂$ between normed vector spaces $V$ and $V₂$ over a normed field $\mathbb{K}$, the underlying linear isometric equivalence of the corresponding affine isometric equivalence $e.toAffineIsometryEquiv$ is equal to $e$ itself.

LinearIsometryEquiv.toAffineIsometryEquiv_toAffineEquiv theorem

: e.toAffineIsometryEquiv.toAffineEquiv = e.toLinearEquiv.toAffineEquiv

Full source

@[simp]
theorem toAffineIsometryEquiv_toAffineEquiv :
    e.toAffineIsometryEquiv.toAffineEquiv = e.toLinearEquiv.toAffineEquiv :=
  rfl

Affine equivalence compatibility of linear isometric equivalence to affine isometric equivalence

Informal description

For a linear isometric equivalence $e : V \simeq_{li}[\mathbb{K}] V₂$ between normed vector spaces $V$ and $V₂$ over a normed field $\mathbb{K}$, the underlying affine equivalence of the induced affine isometric equivalence $e.toAffineIsometryEquiv$ coincides with the affine equivalence induced by the underlying linear equivalence of $e$. That is, $e.toAffineIsometryEquiv.toAffineEquiv = e.toLinearEquiv.toAffineEquiv$.

LinearIsometryEquiv.toAffineIsometryEquiv_toAffineIsometry theorem

: e.toAffineIsometryEquiv.toAffineIsometry = e.toLinearIsometry.toAffineIsometry

Full source

@[simp]
theorem toAffineIsometryEquiv_toAffineIsometry :
    e.toAffineIsometryEquiv.toAffineIsometry = e.toLinearIsometry.toAffineIsometry :=
  rfl

Equality of Affine Isometric Embeddings from Linear Isometric Equivalence

Informal description

For any linear isometric equivalence $e$ between normed vector spaces $V$ and $V₂$ over a normed field $\mathbb{K}$, the underlying affine isometric embedding of the corresponding affine isometric equivalence $e'$ (constructed from $e$) is equal to the affine isometric embedding obtained from the linear isometry corresponding to $e$.

AffineIsometryEquiv.isometry theorem

: Isometry e

Full source

protected theorem isometry : Isometry e :=
  e.toAffineIsometry.isometry

Affine Isometric Equivalence Preserves Distance

Informal description

An affine isometric equivalence $e \colon P \to P₂$ between normed affine spaces is an isometry, meaning it preserves distances between points in the metric space.

AffineIsometryEquiv.toIsometryEquiv definition

: P ≃ᵢ P₂

Full source

/-- Reinterpret an `AffineIsometryEquiv` as an `IsometryEquiv`. -/
def toIsometryEquiv : P ≃ᵢ P₂ :=
  ⟨e.toAffineEquiv.toEquiv, e.isometry⟩

Affine isometric equivalence as isometric equivalence

Informal description

The function converts an affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces into an isometric equivalence $P \simeq^i P₂$ of metric spaces, preserving the distance between points.

AffineIsometryEquiv.coe_toIsometryEquiv theorem

: ⇑e.toIsometryEquiv = e

Full source

@[simp]
theorem coe_toIsometryEquiv : ⇑e.toIsometryEquiv = e :=
  rfl

Underlying Function of Affine Isometric Equivalence Matches Its Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$, the underlying function of the corresponding isometric equivalence $e.\text{toIsometryEquiv}$ is equal to $e$ itself.

AffineIsometryEquiv.range_eq_univ theorem

(e : P ≃ᵃⁱ[𝕜] P₂) : Set.range e = Set.univ

Full source

theorem range_eq_univ (e : P ≃ᵃⁱ[𝕜] P₂) : Set.range e = Set.univ := by
  rw [← coe_toIsometryEquiv]
  exact IsometryEquiv.range_eq_univ _

Affine Isometric Equivalence is Surjective

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, the range of $e$ is equal to the entire space $P₂$, i.e., $\text{range}(e) = \text{univ}$.

AffineIsometryEquiv.toHomeomorph definition

: P ≃ₜ P₂

Full source

/-- Reinterpret an `AffineIsometryEquiv` as a `Homeomorph`. -/
def toHomeomorph : P ≃ₜ P₂ :=
  e.toIsometryEquiv.toHomeomorph

Affine isometric equivalence as homeomorphism

Informal description

The function converts an affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces into a homeomorphism $P \simeq^t P₂$ of topological spaces, preserving the topological structure.

AffineIsometryEquiv.coe_toHomeomorph theorem

: ⇑e.toHomeomorph = e

Full source

@[simp]
theorem coe_toHomeomorph : ⇑e.toHomeomorph = e :=
  rfl

Homeomorphism Underlying Function of Affine Isometric Equivalence

Informal description

For an affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$, the underlying function of the homeomorphism $e.toHomeomorph$ is equal to $e$ itself.

AffineIsometryEquiv.continuous theorem

: Continuous e

Full source

protected theorem continuous : Continuous e :=
  e.isometry.continuous

Continuity of Affine Isometric Equivalence

Informal description

An affine isometric equivalence $e \colon P \to P₂$ between normed affine spaces is continuous.

AffineIsometryEquiv.continuousAt theorem

{x} : ContinuousAt e x

Full source

protected theorem continuousAt {x} : ContinuousAt e x :=
  e.continuous.continuousAt

Pointwise Continuity of Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \to P₂$ between normed affine spaces and any point $x \in P$, the map $e$ is continuous at $x$.

AffineIsometryEquiv.continuousOn theorem

{s} : ContinuousOn e s

Full source

protected theorem continuousOn {s} : ContinuousOn e s :=
  e.continuous.continuousOn

Continuity of Affine Isometric Equivalence on Subsets

Informal description

For any affine isometric equivalence $e \colon P \to P₂$ between normed affine spaces over a normed field $\mathbb{K}$, and for any subset $s \subseteq P$, the restriction of $e$ to $s$ is continuous on $s$.

AffineIsometryEquiv.continuousWithinAt theorem

{s x} : ContinuousWithinAt e s x

Full source

protected theorem continuousWithinAt {s x} : ContinuousWithinAt e s x :=
  e.continuous.continuousWithinAt

Continuity Within Subset for Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \to P₂$ between normed affine spaces over a normed field $\mathbb{K}$, and for any subset $s \subseteq P$ and point $x \in P$, the map $e$ is continuous within $s$ at $x$.

AffineIsometryEquiv.refl definition

: P ≃ᵃⁱ[𝕜] P

Full source

/-- Identity map as an `AffineIsometryEquiv`. -/
def refl : P ≃ᵃⁱ[𝕜] P :=
  ⟨AffineEquiv.refl 𝕜 P, fun _ => rfl⟩

Identity affine isometric equivalence

Informal description

The identity map on a normed vector space $P$ over a normed field $\mathbb{K}$, viewed as an affine isometric equivalence from $P$ to itself. This map preserves both the affine structure and the distance between points.

AffineIsometryEquiv.instInhabited instance

: Inhabited (P ≃ᵃⁱ[𝕜] P)

Full source

instance : Inhabited (P ≃ᵃⁱ[𝕜] P) :=
  ⟨refl 𝕜 P⟩

Inhabited Type of Affine Isometric Self-Equivalences

Informal description

For any normed vector space $P$ over a normed field $\mathbb{K}$, the type of affine isometric equivalences $P \simeq^{ai}[\mathbb{K}] P$ is inhabited, with the identity map as a canonical element.

AffineIsometryEquiv.coe_refl theorem

: ⇑(refl 𝕜 P) = id

Full source

@[simp]
theorem coe_refl : ⇑(refl 𝕜 P) = id :=
  rfl

Identity Affine Isometric Equivalence as Identity Function

Informal description

The underlying function of the identity affine isometric equivalence on a normed vector space $P$ over a normed field $\mathbb{K}$ is equal to the identity function, i.e., $\text{refl}_{\mathbb{K}} P = \text{id}$.

AffineIsometryEquiv.toAffineEquiv_refl theorem

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

Full source

@[simp]
theorem toAffineEquiv_refl : (refl 𝕜 P).toAffineEquiv = AffineEquiv.refl 𝕜 P :=
  rfl

Identity Affine Isometric Equivalence Yields Identity Affine Equivalence

Informal description

The underlying affine equivalence of the identity affine isometric equivalence on $P$ is equal to the identity affine equivalence on $P$.

AffineIsometryEquiv.toIsometryEquiv_refl theorem

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

Full source

@[simp]
theorem toIsometryEquiv_refl : (refl 𝕜 P).toIsometryEquiv = IsometryEquiv.refl P :=
  rfl

Identity Affine Isometric Equivalence Yields Identity Isometric Equivalence

Informal description

The isometric equivalence obtained from the identity affine isometric equivalence on a normed space $P$ over a field $\mathbb{K}$ is equal to the identity isometric equivalence on $P$.

AffineIsometryEquiv.toHomeomorph_refl theorem

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

Full source

@[simp]
theorem toHomeomorph_refl : (refl 𝕜 P).toHomeomorph = Homeomorph.refl P :=
  rfl

Identity Affine Isometric Equivalence Yields Identity Homeomorphism

Informal description

The homeomorphism obtained from the identity affine isometric equivalence on a normed space $P$ over a field $\mathbb{K}$ is equal to the identity homeomorphism on $P$.

AffineIsometryEquiv.symm definition

: P₂ ≃ᵃⁱ[𝕜] P

Full source

/-- The inverse `AffineIsometryEquiv`. -/
def symm : P₂ ≃ᵃⁱ[𝕜] P :=
  { e.toAffineEquiv.symm with norm_map := e.linearIsometryEquiv.symm.norm_map }

Inverse affine isometric equivalence

Informal description

The inverse of an affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ is an affine isometric equivalence $e^{-1} : P₂ \simeq^{ai}[\mathbb{K}] P$ that preserves distances and reverses the direction of the original map.

AffineIsometryEquiv.apply_symm_apply theorem

(x : P₂) : e (e.symm x) = x

Full source

@[simp]
theorem apply_symm_apply (x : P₂) : e (e.symm x) = x :=
  e.toAffineEquiv.apply_symm_apply x

Affine Isometric Equivalence: $e(e^{-1}(x)) = x$

Informal description

For any affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ and any point $x \in P₂$, applying $e$ to the inverse image of $x$ under $e$ yields $x$ itself, i.e., $e(e^{-1}(x)) = x$.

AffineIsometryEquiv.symm_apply_apply theorem

(x : P) : e.symm (e x) = x

Full source

@[simp]
theorem symm_apply_apply (x : P) : e.symm (e x) = x :=
  e.toAffineEquiv.symm_apply_apply x

Inverse of Affine Isometric Equivalence Cancels Original Map

Informal description

For any affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ and any point $x \in P$, the composition of $e$ with its inverse $e^{-1}$ satisfies $e^{-1}(e(x)) = x$.

AffineIsometryEquiv.symm_symm theorem

: e.symm.symm = e

Full source

@[simp]
theorem symm_symm : e.symm.symm = e := rfl

Double Inverse of Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$, the inverse of its inverse is equal to $e$ itself, i.e., $(e^{-1})^{-1} = e$.

AffineIsometryEquiv.symm_bijective theorem

: Bijective (AffineIsometryEquiv.symm : (P₂ ≃ᵃⁱ[𝕜] P) → _)

Full source

theorem symm_bijective : Bijective (AffineIsometryEquiv.symm : (P₂ ≃ᵃⁱ[𝕜] P) → _) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Affine Isometric Equivalences

Informal description

The inverse operation on affine isometric equivalences, which maps an equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ to its inverse $e^{-1} : P₂ \simeq^{ai}[\mathbb{K}] P$, is a bijective function.

AffineIsometryEquiv.toAffineEquiv_symm theorem

: e.toAffineEquiv.symm = e.symm.toAffineEquiv

Full source

@[simp]
theorem toAffineEquiv_symm : e.toAffineEquiv.symm = e.symm.toAffineEquiv :=
  rfl

Inverse of Underlying Affine Equivalence in Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$, the inverse of its underlying affine equivalence $e.\text{toAffineEquiv}$ is equal to the underlying affine equivalence of its inverse $e.\text{symm}.\text{toAffineEquiv}$.

AffineIsometryEquiv.toIsometryEquiv_symm theorem

: e.toIsometryEquiv.symm = e.symm.toIsometryEquiv

Full source

@[simp]
theorem toIsometryEquiv_symm : e.toIsometryEquiv.symm = e.symm.toIsometryEquiv :=
  rfl

Inverse of Isometric Equivalence Associated with Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$, the inverse of its associated isometric equivalence $e.\text{toIsometryEquiv}$ is equal to the isometric equivalence associated with its inverse $e.\text{symm}.\text{toIsometryEquiv}$.

AffineIsometryEquiv.toHomeomorph_symm theorem

: e.toHomeomorph.symm = e.symm.toHomeomorph

Full source

@[simp]
theorem toHomeomorph_symm : e.toHomeomorph.symm = e.symm.toHomeomorph :=
  rfl

Inverse of Homeomorphism from Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$, the inverse of the homeomorphism associated with $e$ is equal to the homeomorphism associated with the inverse of $e$.

AffineIsometryEquiv.trans definition

(e' : P₂ ≃ᵃⁱ[𝕜] P₃) : P ≃ᵃⁱ[𝕜] P₃

Full source

/-- Composition of `AffineIsometryEquiv`s as an `AffineIsometryEquiv`. -/
def trans (e' : P₂ ≃ᵃⁱ[𝕜] P₃) : P ≃ᵃⁱ[𝕜] P₃ :=
  ⟨e.toAffineEquiv.trans e'.toAffineEquiv, fun _ => (e'.norm_map _).trans (e.norm_map _)⟩

Composition of affine isometric equivalences

Informal description

Given affine isometric equivalences $e : P \simeq^{ai}[\mathbb{K}] P₂$ and $e' : P₂ \simeq^{ai}[\mathbb{K}] P₃$, the composition $e \circ e'$ is an affine isometric equivalence from $P$ to $P₃$ over the normed field $\mathbb{K}$. This composition preserves distances, i.e., it satisfies $\|e \circ e'(x) - e \circ e'(y)\| = \|x - y\|$ for all $x, y \in P$.

AffineIsometryEquiv.coe_trans theorem

(e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁

Full source

@[simp]
theorem coe_trans (e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ :=
  rfl

Composition of Affine Isometric Equivalences Preserves Function Application

Informal description

For any affine isometric equivalences $e_1 : P \simeq^{ai}[\mathbb{K}] P_2$ and $e_2 : P_2 \simeq^{ai}[\mathbb{K}] P_3$ between normed vector spaces over a normed field $\mathbb{K}$, the underlying function of the composition $e_1 \circ e_2$ is equal to the composition of the underlying functions, i.e., $(e_1 \circ e_2)(x) = e_2(e_1(x))$ for all $x \in P$.

AffineIsometryEquiv.trans_refl theorem

: e.trans (refl 𝕜 P₂) = e

Full source

@[simp]
theorem trans_refl : e.trans (refl 𝕜 P₂) = e :=
  ext fun _ => rfl

Composition with Identity Preserves Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces over a normed field $\mathbb{K}$, the composition of $e$ with the identity affine isometric equivalence on $P₂$ is equal to $e$ itself, i.e., $e \circ \text{id}_{P₂} = e$.

AffineIsometryEquiv.refl_trans theorem

: (refl 𝕜 P).trans e = e

Full source

@[simp]
theorem refl_trans : (refl 𝕜 P).trans e = e :=
  ext fun _ => rfl

Identity Composition Property of Affine Isometric Equivalences

Informal description

For any affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, the composition of the identity affine isometric equivalence on $P$ with $e$ is equal to $e$ itself. In other words, $(id_P) \circ e = e$.

AffineIsometryEquiv.self_trans_symm theorem

: e.trans e.symm = refl 𝕜 P

Full source

@[simp]
theorem self_trans_symm : e.trans e.symm = refl 𝕜 P :=
  ext e.symm_apply_apply

Composition of Affine Isometric Equivalence with Its Inverse Yields Identity

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P_2$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity affine isometric equivalence on $P$.

AffineIsometryEquiv.symm_trans_self theorem

: e.symm.trans e = refl 𝕜 P₂

Full source

@[simp]
theorem symm_trans_self : e.symm.trans e = refl 𝕜 P₂ :=
  ext e.apply_symm_apply

Inverse Composition Yields Identity: $e^{-1} \circ e = \text{id}_{P₂}$

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$, the composition of its inverse $e^{-1}$ with $e$ itself equals the identity affine isometric equivalence on $P₂$.

AffineIsometryEquiv.coe_symm_trans theorem

 (e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) : ⇑(e₁.trans e₂).symm = e₁.symm ∘ e₂.symm

Full source

@[simp]
theorem coe_symm_trans (e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) :
    ⇑(e₁.trans e₂).symm = e₁.symm ∘ e₂.symm :=
  rfl

Inverse of Composition of Affine Isometric Equivalences

Informal description

For any affine isometric equivalences $e_1 \colon P \simeq^{ai}[\mathbb{K}] P_2$ and $e_2 \colon P_2 \simeq^{ai}[\mathbb{K}] P_3$, the underlying function of the inverse of their composition $(e_1 \circ e_2)^{-1}$ is equal to the composition of their inverses $e_2^{-1} \circ e_1^{-1}$.

AffineIsometryEquiv.trans_assoc theorem

 (ePP₂ : P ≃ᵃⁱ[𝕜] P₂) (eP₂G : P₂ ≃ᵃⁱ[𝕜] P₃) (eGG' : P₃ ≃ᵃⁱ[𝕜] P₄) :
  ePP₂.trans (eP₂G.trans eGG') = (ePP₂.trans eP₂G).trans eGG'

Full source

theorem trans_assoc (ePP₂ : P ≃ᵃⁱ[𝕜] P₂) (eP₂G : P₂ ≃ᵃⁱ[𝕜] P₃) (eGG' : P₃ ≃ᵃⁱ[𝕜] P₄) :
    ePP₂.trans (eP₂G.trans eGG') = (ePP₂.trans eP₂G).trans eGG' :=
  rfl

Associativity of Composition of Affine Isometric Equivalences

Informal description

For any affine isometric equivalences $e_{PP₂} : P \simeq^{ai}[\mathbb{K}] P₂$, $e_{P₂G} : P₂ \simeq^{ai}[\mathbb{K}] P₃$, and $e_{GG'} : P₃ \simeq^{ai}[\mathbb{K}] P₄$, the composition of these equivalences is associative. That is, composing $e_{PP₂}$ with the composition of $e_{P₂G}$ and $e_{GG'}$ is equal to composing the composition of $e_{PP₂}$ and $e_{P₂G}$ with $e_{GG'}$.

AffineIsometryEquiv.instGroup instance

: Group (P ≃ᵃⁱ[𝕜] P)

Full source

/-- The group of affine isometries of a `NormedAddTorsor`, `P`. -/
instance instGroup : Group (P ≃ᵃⁱ[𝕜] P) where
  mul e₁ e₂ := e₂.trans e₁
  one := refl _ _
  inv := symm
  one_mul := trans_refl
  mul_one := refl_trans
  mul_assoc _ _ _ := trans_assoc _ _ _
  inv_mul_cancel := self_trans_symm

Group Structure of Affine Isometric Self-Equivalences

Informal description

The set of affine isometric self-equivalences $P \simeq^{ai}[\mathbb{K}] P$ on a normed affine space $P$ over a normed field $\mathbb{K}$ forms a group under composition. This group structure includes the identity map as the neutral element, the inverse operation given by taking the inverse affine isometric equivalence, and the group operation given by composition of maps.

AffineIsometryEquiv.coe_one theorem

: ⇑(1 : P ≃ᵃⁱ[𝕜] P) = id

Full source

@[simp]
theorem coe_one : ⇑(1 : P ≃ᵃⁱ[𝕜] P) = id :=
  rfl

Identity Affine Isometric Self-Equivalence is the Identity Function

Informal description

The identity affine isometric self-equivalence on a normed affine space $P$ over a normed field $\mathbb{K}$, denoted by $1 : P \simeq^{ai}[\mathbb{K}] P$, is equal to the identity function $\text{id} : P \to P$.

AffineIsometryEquiv.coe_mul theorem

(e e' : P ≃ᵃⁱ[𝕜] P) : ⇑(e * e') = e ∘ e'

Full source

@[simp]
theorem coe_mul (e e' : P ≃ᵃⁱ[𝕜] P) : ⇑(e * e') = e ∘ e' :=
  rfl

Composition of Affine Isometric Self-Equivalences as Function Composition

Informal description

For any two affine isometric self-equivalences $e, e' \colon P \simeq^{ai}[\mathbb{K}] P$ on a normed affine space $P$ over a normed field $\mathbb{K}$, the composition of $e$ and $e'$ as group elements equals the function composition of $e$ and $e'$, i.e., $(e * e')(p) = e(e'(p))$ for all $p \in P$.

AffineIsometryEquiv.coe_inv theorem

(e : P ≃ᵃⁱ[𝕜] P) : ⇑e⁻¹ = e.symm

Full source

@[simp]
theorem coe_inv (e : P ≃ᵃⁱ[𝕜] P) : ⇑e⁻¹ = e.symm :=
  rfl

Inverse of Affine Isometric Self-Equivalence Equals Its Symmetric

Informal description

For any affine isometric self-equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P$ on a normed affine space $P$ over a normed field $\mathbb{K}$, the inverse map $e^{-1}$ is equal to the symmetric affine isometric equivalence $e.symm \colon P \simeq^{ai}[\mathbb{K}] P$.

AffineIsometryEquiv.map_vadd theorem

(p : P) (v : V) : e (v +ᵥ p) = e.linearIsometryEquiv v +ᵥ e p

Full source

@[simp]
theorem map_vadd (p : P) (v : V) : e (v +ᵥ p) = e.linearIsometryEquiv v +ᵥ e p :=
  e.toAffineIsometry.map_vadd p v

Affine Isometric Equivalence Preserves Vector Addition

Informal description

For an affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, a point $p \in P$, and a vector $v \in V$, the action of $e$ on the sum $v + p$ is given by $e(v + p) = e.linearIsometryEquiv(v) + e(p)$, where $e.linearIsometryEquiv$ is the underlying linear isometric equivalence of $e$.

AffineIsometryEquiv.map_vsub theorem

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

Full source

@[simp]
theorem map_vsub (p1 p2 : P) : e.linearIsometryEquiv (p1 -ᵥ p2) = e p1 -ᵥ e p2 :=
  e.toAffineIsometry.map_vsub p1 p2

Affine Isometric Equivalence Preserves Vector Difference

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$ between normed affine spaces $P$ and $P₂$ over a normed field $\mathbb{K}$, and any two points $p₁, p₂ \in P$, the linear isometric equivalence underlying $e$ applied to the vector difference $p₁ - p₂$ equals the vector difference of the images $e(p₁) - e(p₂)$ in $P₂$.

AffineIsometryEquiv.dist_map theorem

(x y : P) : dist (e x) (e y) = dist x y

Full source

@[simp]
theorem dist_map (x y : P) : dist (e x) (e y) = dist x y :=
  e.toAffineIsometry.dist_map x y

Distance Preservation under Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$ and any two points $x, y \in P$, the distance between $e(x)$ and $e(y)$ in $P₂$ is equal to the distance between $x$ and $y$ in $P$, i.e., $\operatorname{dist}(e(x), e(y)) = \operatorname{dist}(x, y)$.

AffineIsometryEquiv.edist_map theorem

(x y : P) : edist (e x) (e y) = edist x y

Full source

@[simp]
theorem edist_map (x y : P) : edist (e x) (e y) = edist x y :=
  e.toAffineIsometry.edist_map x y

Extended Distance Preservation under Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \simeq^{ai}[\mathbb{K}] P₂$ and any two points $x, y \in P$, the extended distance between $e(x)$ and $e(y)$ in $P₂$ is equal to the extended distance between $x$ and $y$ in $P$, i.e., $\operatorname{edist}(e(x), e(y)) = \operatorname{edist}(x, y)$.

AffineIsometryEquiv.bijective theorem

: Bijective e

Full source

protected theorem bijective : Bijective e :=
  e.1.bijective

Bijectivity of Affine Isometric Equivalence

Informal description

An affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ is bijective, meaning it is both injective and surjective.

AffineIsometryEquiv.injective theorem

: Injective e

Full source

protected theorem injective : Injective e :=
  e.1.injective

Injectivity of Affine Isometric Equivalence

Informal description

An affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ is injective, meaning that for any $x, y \in P$, if $e(x) = e(y)$, then $x = y$.

AffineIsometryEquiv.surjective theorem

: Surjective e

Full source

protected theorem surjective : Surjective e :=
  e.1.surjective

Surjectivity of Affine Isometric Equivalence

Informal description

An affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ is surjective, meaning that for every point $y \in P₂$, there exists a point $x \in P$ such that $e(x) = y$.

AffineIsometryEquiv.map_eq_iff theorem

{x y : P} : e x = e y ↔ x = y

Full source

theorem map_eq_iff {x y : P} : e x = e y ↔ x = y :=
  e.injective.eq_iff

Affine Isometric Equivalence Preserves Distinctness

Informal description

For an affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ and any points $x, y \in P$, the images $e(x)$ and $e(y)$ are equal if and only if $x = y$.

AffineIsometryEquiv.map_ne theorem

{x y : P} (h : x ≠ y) : e x ≠ e y

Full source

theorem map_ne {x y : P} (h : x ≠ y) : e x ≠ e y :=
  e.injective.ne h

Affine Isometric Equivalence Preserves Inequality

Informal description

For any affine isometric equivalence $e : P \simeq^{ai}[\mathbb{K}] P₂$ and any points $x, y \in P$ with $x \neq y$, the images $e(x)$ and $e(y)$ are distinct, i.e., $e(x) \neq e(y)$.

AffineIsometryEquiv.lipschitz theorem

: LipschitzWith 1 e

Full source

protected theorem lipschitz : LipschitzWith 1 e :=
  e.isometry.lipschitz

Affine Isometric Equivalence is 1-Lipschitz

Informal description

An affine isometric equivalence $e \colon P \to P₂$ is a Lipschitz map with constant $1$, i.e., for any $x, y \in P$, the distance between $e(x)$ and $e(y)$ is less than or equal to the distance between $x$ and $y$.

AffineIsometryEquiv.antilipschitz theorem

: AntilipschitzWith 1 e

Full source

protected theorem antilipschitz : AntilipschitzWith 1 e :=
  e.isometry.antilipschitz

Affine Isometric Equivalence is Antilipschitz with Constant 1

Informal description

An affine isometric equivalence $e \colon P \to P₂$ is antilipschitz with constant $1$, meaning that for any two points $x, y \in P$, the distance between $x$ and $y$ is bounded below by the distance between their images under $e$, i.e., $\text{dist}(x, y) \leq \text{dist}(e(x), e(y))$.

AffineIsometryEquiv.ediam_image theorem

(s : Set P) : EMetric.diam (e '' s) = EMetric.diam s

Full source

@[simp]
theorem ediam_image (s : Set P) : EMetric.diam (e '' s) = EMetric.diam s :=
  e.isometry.ediam_image s

Preservation of Extended Metric Diameter under Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \to P₂$ between normed affine spaces and any subset $s \subseteq P$, the extended metric diameter of the image $e(s)$ is equal to the extended metric diameter of $s$, i.e., $\text{diam}(e(s)) = \text{diam}(s)$.

AffineIsometryEquiv.diam_image theorem

(s : Set P) : Metric.diam (e '' s) = Metric.diam s

Full source

@[simp]
theorem diam_image (s : Set P) : Metric.diam (e '' s) = Metric.diam s :=
  e.isometry.diam_image s

Preservation of Diameter under Affine Isometric Equivalence

Informal description

For any affine isometric equivalence $e \colon P \to P₂$ between normed affine spaces and any subset $s \subseteq P$, the diameter of the image $e(s)$ is equal to the diameter of $s$, i.e., $\text{diam}(e(s)) = \text{diam}(s)$.

AffineIsometryEquiv.comp_continuousOn_iff theorem

{f : α → P} {s : Set α} : ContinuousOn (e ∘ f) s ↔ ContinuousOn f s

Full source

@[simp]
theorem comp_continuousOn_iff {f : α → P} {s : Set α} : ContinuousOnContinuousOn (e ∘ f) s ↔ ContinuousOn f s :=
  e.isometry.comp_continuousOn_iff

Continuity of Composition with Affine Isometric Equivalence

Informal description

Let $e \colon P \to P_2$ be an affine isometric equivalence between normed affine spaces over a normed field $\mathbb{K}$. For any function $f \colon \alpha \to P$ and subset $s \subseteq \alpha$, the composition $e \circ f$ is continuous on $s$ if and only if $f$ is continuous on $s$.

AffineIsometryEquiv.comp_continuous_iff theorem

{f : α → P} : Continuous (e ∘ f) ↔ Continuous f

Full source

@[simp]
theorem comp_continuous_iff {f : α → P} : ContinuousContinuous (e ∘ f) ↔ Continuous f :=
  e.isometry.comp_continuous_iff

Continuity of Composition with Affine Isometric Equivalence

Informal description

For any function $f \colon \alpha \to P$ from a topological space $\alpha$ to a normed affine space $P$, the composition $e \circ f$ is continuous if and only if $f$ is continuous, where $e \colon P \to P$ is an affine isometric equivalence.

AffineIsometryEquiv.ofTop definition

(h : s₁ = ⊤) : s₁ ≃ᵃⁱ[𝕜] P

Full source

/-- The identity equivalence of an affine subspace equal to `⊤` to the whole space. -/
def ofTop (h : s₁ = ⊤) : s₁ ≃ᵃⁱ[𝕜] P :=
  { (AffineEquiv.ofEq s₁ ⊤ h).trans (AffineSubspace.topEquiv 𝕜 V P) with norm_map := fun _ ↦ rfl }

Identity affine isometric equivalence for the whole space

Informal description

Given an affine subspace $s₁$ of a normed vector space $P$ over a normed field $\mathbb{K}$, if $s₁$ is equal to the entire space (i.e., $s₁ = \top$), then the identity map from $s₁$ to $P$ is an affine isometric equivalence. This means it preserves both the affine structure and the distance between points.

AffineIsometryEquiv.ofTop_apply theorem

(h : s₁ = ⊤) (x : s₁) : (ofTop s₁ h x : P) = x

Full source

@[simp]
lemma ofTop_apply (h : s₁ = ⊤) (x : s₁) : (ofTop s₁ h x : P) = x :=
  rfl

Identity Affine Isometric Equivalence Preserves Points in the Whole Space

Informal description

For any affine subspace $s₁$ of a normed vector space $P$ over a normed field $\mathbb{K}$, if $s₁$ is equal to the entire space (i.e., $s₁ = \top$), then the application of the identity affine isometric equivalence `ofTop` to any point $x \in s₁$ yields $x$ itself when viewed as an element of $P$. In other words, $(ofTop\, s₁\, h)(x) = x$ for all $x \in s₁$.

AffineIsometryEquiv.ofTop_symm_apply_coe theorem

(h : s₁ = ⊤) (x : P) : (ofTop s₁ h).symm x = x

Full source

@[simp]
lemma ofTop_symm_apply_coe (h : s₁ = ⊤) (x : P) : (ofTop s₁ h).symm x = x :=
  rfl

Inverse of Identity Affine Isometric Equivalence Acts as Identity on Points

Informal description

For any affine subspace $s₁$ of a normed vector space $P$ over a normed field $\mathbb{K}$, if $s₁$ is equal to the entire space (i.e., $s₁ = \top$), then the inverse of the identity affine isometric equivalence $(ofTop\, s₁\, h)^{-1}$ maps any point $x \in P$ to itself, i.e., $(ofTop\, s₁\, h)^{-1}(x) = x$.

AffineIsometryEquiv.ofEq definition

(h : s₁ = s₂) : s₁ ≃ᵃⁱ[𝕜] s₂

Full source

/-- `AffineEquiv.ofEq` as an `AffineIsometryEquiv`. -/
def ofEq (h : s₁ = s₂) : s₁ ≃ᵃⁱ[𝕜] s₂ :=
  { AffineEquiv.ofEq s₁ s₂ h with norm_map := fun _ ↦ rfl }

Affine isometric equivalence induced by equality of subsets

Informal description

Given two subsets $s_1$ and $s_2$ of a normed space $P$ over a field $\mathbb{K}$, and an equality $h : s_1 = s_2$, the function constructs an affine isometric equivalence between $s_1$ and $s_2$. This equivalence preserves distances and is defined by the identity map on the underlying space $P$.

AffineIsometryEquiv.coe_ofEq_apply theorem

(h : s₁ = s₂) (x : s₁) : (ofEq s₁ s₂ h x : P) = x

Full source

@[simp]
lemma coe_ofEq_apply (h : s₁ = s₂) (x : s₁) : (ofEq s₁ s₂ h x : P) = x :=
  rfl

Image under Affine Isometric Equivalence Induced by Subset Equality

Informal description

Given two subsets $s_1$ and $s_2$ of a normed space $P$ over a field $\mathbb{K}$ with $h : s_1 = s_2$, for any $x \in s_1$, the image of $x$ under the affine isometric equivalence $\text{ofEq}\, s_1\, s_2\, h$ (when viewed as an element of $P$) equals $x$ itself.

AffineIsometryEquiv.ofEq_symm theorem

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

Full source

@[simp]
lemma ofEq_symm (h : s₁ = s₂) : (ofEq s₁ s₂ h).symm = ofEq s₂ s₁ h.symm :=
  rfl

Inverse of Affine Isometric Equivalence Induced by Equality

Informal description

Given two subsets $s_1$ and $s_2$ of a normed space $P$ over a field $\mathbb{K}$ and an equality $h : s_1 = s_2$, the inverse of the affine isometric equivalence constructed from $h$ is equal to the affine isometric equivalence constructed from the symmetric equality $h^{-1} : s_2 = s_1$.

AffineIsometryEquiv.ofEq_rfl theorem

: ofEq s₁ s₁ rfl = refl 𝕜 s₁

Full source

@[simp]
lemma ofEq_rfl : ofEq s₁ s₁ rfl = refl 𝕜 s₁ :=
  rfl

Identity Affine Isometric Equivalence from Reflexivity Equality

Informal description

The affine isometric equivalence constructed from the reflexivity equality $s_1 = s_1$ is equal to the identity affine isometric equivalence on $s_1$.

AffineIsometryEquiv.vaddConst definition

(p : P) : V ≃ᵃⁱ[𝕜] P

Full source

/-- The map `v ↦ v +ᵥ p` as an affine isometric equivalence between `V` and `P`. -/
def vaddConst (p : P) : V ≃ᵃⁱ[𝕜] P :=
  { AffineEquiv.vaddConst 𝕜 p with norm_map := fun _ => rfl }

Affine isometric equivalence by vector addition

Informal description

For a given point $ p $ in an affine space $ P $ over a normed vector space $ V $, the map $ v \mapsto v + p $ defines an affine isometric equivalence between $ V $ and $ P $. This map preserves distances, meaning that the distance between any two vectors $ v_1 $ and $ v_2 $ in $ V $ is equal to the distance between their corresponding points $ v_1 + p $ and $ v_2 + p $ in $ P $.

AffineIsometryEquiv.coe_vaddConst theorem

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

Full source

@[simp]
theorem coe_vaddConst (p : P) : ⇑(vaddConst 𝕜 p) = fun v => v +ᵥ p :=
  rfl

Function Representation of Vector Addition Affine Isometric Equivalence

Informal description

For any point $p$ in an affine space $P$ over a normed vector space $V$ with scalar field $\mathbb{K}$, the function representation of the affine isometric equivalence `vaddConst 𝕜 p` is given by the map $v \mapsto v + p$ for all $v \in V$.

AffineIsometryEquiv.coe_vaddConst' theorem

(p : P) : ↑(AffineEquiv.vaddConst 𝕜 p) = fun v => v +ᵥ p

Full source

@[simp]
theorem coe_vaddConst' (p : P) : ↑(AffineEquiv.vaddConst 𝕜 p) = fun v => v +ᵥ p :=
  rfl

Coercion of Vector Addition Affine Isometric Equivalence

Informal description

For any point $p$ in an affine space $P$, the coercion of the affine isometric equivalence `AffineEquiv.vaddConst 𝕜 p` is equal to the function that maps a vector $v$ to the point obtained by adding $v$ to $p$ (denoted $v +ᵥ p$).

AffineIsometryEquiv.coe_vaddConst_symm theorem

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

Full source

@[simp]
theorem coe_vaddConst_symm (p : P) : ⇑(vaddConst 𝕜 p).symm = fun p' => p' -ᵥ p :=
  rfl

Inverse of Vector Addition Affine Isometric Equivalence: $(v + p)^{-1} = p' - p$

Informal description

For any point $p$ in an affine space $P$ over a normed vector space $V$ with scalar field $\mathbb{K}$, the inverse of the affine isometric equivalence $v \mapsto v + p$ is given by the function $p' \mapsto p' - p$, where $-$ denotes the vector subtraction in the affine space.

AffineIsometryEquiv.vaddConst_toAffineEquiv theorem

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

Full source

@[simp]
theorem vaddConst_toAffineEquiv (p : P) :
    (vaddConst 𝕜 p).toAffineEquiv = AffineEquiv.vaddConst 𝕜 p :=
  rfl

Underlying Affine Equivalence of Vector Addition Isometric Equivalence

Informal description

For any point $p$ in an affine space $P$ over a normed vector space $V$, the underlying affine equivalence of the affine isometric equivalence `vaddConst 𝕜 p` is equal to the affine equivalence `AffineEquiv.vaddConst 𝕜 p`.

AffineIsometryEquiv.constVSub definition

(p : P) : P ≃ᵃⁱ[𝕜] V

Full source

/-- `p' ↦ p -ᵥ p'` as an affine isometric equivalence. -/
def constVSub (p : P) : P ≃ᵃⁱ[𝕜] V :=
  { AffineEquiv.constVSub 𝕜 p with norm_map := norm_neg }

Affine isometric equivalence by subtraction from a fixed point

Informal description

For a fixed point $ p $ in a normed affine space $ P $ over a normed field $ \mathbb{K} $, the map $ p' \mapsto p -ᵥ p' $ defines an affine isometric equivalence between $ P $ and the underlying normed vector space $ V $. Here, $ -ᵥ $ denotes the subtraction operation in the affine space.

AffineIsometryEquiv.coe_constVSub theorem

(p : P) : ⇑(constVSub 𝕜 p) = (p -ᵥ ·)

Full source

@[simp]
theorem coe_constVSub (p : P) : ⇑(constVSub 𝕜 p) = (p -ᵥ ·) :=
  rfl

Explicit form of the affine isometric equivalence by subtraction from a fixed point

Informal description

For a fixed point $p$ in a normed affine space $P$ over a normed field $\mathbb{K}$, the map $\text{constVSub}_{\mathbb{K}}(p) : P \to V$ is given by $p' \mapsto p -ᵥ p'$, where $-ᵥ$ denotes the subtraction operation in the affine space.

AffineIsometryEquiv.symm_constVSub theorem

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

Full source

@[simp]
theorem symm_constVSub (p : P) :
    (constVSub 𝕜 p).symm =
      (LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (vaddConst 𝕜 p) := by
  ext
  rfl

Inverse of Affine Isometric Equivalence via Point Subtraction as Composition of Negation and Translation

Informal description

For any point $p$ in a normed affine space $P$ over a normed field $\mathbb{K}$, the inverse of the affine isometric equivalence $\text{constVSub}_{\mathbb{K}}(p) : P \simeq^{ai}[\mathbb{K}] V$ (defined by $p' \mapsto p -ᵥ p'$) is equal to the composition of the affine isometric equivalence induced by the negation linear isometry on $V$ with the translation equivalence $\text{vaddConst}_{\mathbb{K}}(p) : V \simeq^{ai}[\mathbb{K}] P$ (defined by $v \mapsto v + p$).

AffineIsometryEquiv.constVAdd definition

(v : V) : P ≃ᵃⁱ[𝕜] P

Full source

/-- Translation by `v` (that is, the map `p ↦ v +ᵥ p`) as an affine isometric automorphism of `P`.
-/
def constVAdd (v : V) : P ≃ᵃⁱ[𝕜] P :=
  { AffineEquiv.constVAdd 𝕜 P v with norm_map := fun _ => rfl }

Affine isometric automorphism by translation

Informal description

For a vector $ v $ in a normed space $ V $, the map $ p \mapsto v + p $ is an affine isometric automorphism of $ P $, where $ P $ is a normed affine space over $ V $. This means the map preserves distances and is bijective.

AffineIsometryEquiv.coe_constVAdd theorem

(v : V) : ⇑(constVAdd 𝕜 P v : P ≃ᵃⁱ[𝕜] P) = (v +ᵥ ·)

Full source

@[simp]
theorem coe_constVAdd (v : V) : ⇑(constVAdd 𝕜 P v : P ≃ᵃⁱ[𝕜] P) = (v +ᵥ ·) :=
  rfl

Underlying Function of Translation by a Vector in Affine Isometric Automorphism

Informal description

For any vector $v$ in a normed space $V$ over a field $\mathbb{K}$, the underlying function of the affine isometric automorphism `constVAdd 𝕜 P v` (which translates points in the normed affine space $P$ by $v$) is equal to the function that adds $v$ to its argument, i.e., $p \mapsto v + p$.

AffineIsometryEquiv.constVAdd_zero theorem

: constVAdd 𝕜 P (0 : V) = refl 𝕜 P

Full source

@[simp]
theorem constVAdd_zero : constVAdd 𝕜 P (0 : V) = refl 𝕜 P :=
  ext <| zero_vadd V

Translation by Zero Vector is Identity Affine Isometry

Informal description

The affine isometric automorphism given by translation by the zero vector in a normed space $V$ over a field $\mathbb{K}$ is equal to the identity affine isometric equivalence on the normed affine space $P$ over $V$.

AffineIsometryEquiv.vadd_vsub theorem

{f : P → P₂} (hf : Isometry f) {p : P} {g : V → V₂} (hg : ∀ v, g v = f (v +ᵥ p) -ᵥ f p) : Isometry g

Full source

/-- 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. -/
theorem vadd_vsub {f : P → P₂} (hf : Isometry f) {p : P} {g : V → V₂}
    (hg : ∀ v, g v = f (v +ᵥ p) -ᵥ f p) : Isometry g := by
  convert (vaddConst 𝕜 (f p)).symm.isometry.comp (hf.comp (vaddConst 𝕜 p).isometry)
  exact funext hg

Isometry of the linear part of an affine isometry

Informal description

Let $f \colon P \to P₂$ be an isometry between two normed affine spaces, and let $p \in P$ be a base point. Define the map $g \colon V \to V₂$ by $g(v) = f(v + p) - f(p)$ for all $v \in V$, where $V$ and $V₂$ are the underlying vector spaces of $P$ and $P₂$ respectively. Then $g$ is an isometry.

AffineIsometryEquiv.pointReflection definition

(x : P) : P ≃ᵃⁱ[𝕜] P

Full source

/-- Point reflection in `x` as an affine isometric automorphism. -/
def pointReflection (x : P) : P ≃ᵃⁱ[𝕜] P :=
  (constVSub 𝕜 x).trans (vaddConst 𝕜 x)

Point reflection as an affine isometric automorphism

Informal description

For a given point $ x $ in an affine space $ P $ over a normed field $ \mathbb{K} $, the point reflection about $ x $ is an affine isometric automorphism of $ P $. This map sends any point $ y $ to $ x -ᵥ y +ᵥ x $, where $ -ᵥ $ and $ +ᵥ $ denote the subtraction and addition operations in the affine space, respectively. The map preserves distances, meaning that the distance between any two points $ y $ and $ z $ in $ P $ is equal to the distance between their images under the point reflection.

AffineIsometryEquiv.pointReflection_apply theorem

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

Full source

theorem pointReflection_apply (x y : P) : (pointReflection 𝕜 x) y = (x -ᵥ y) +ᵥ x :=
  rfl

Point Reflection Formula in Affine Space

Informal description

For any points $x$ and $y$ in an affine space $P$ over a normed field $\mathbb{K}$, the point reflection of $y$ about $x$ is given by $(x -ᵥ y) +ᵥ x$, where $-ᵥ$ and $+ᵥ$ denote the subtraction and addition operations in the affine space, respectively.

AffineIsometryEquiv.pointReflection_toAffineEquiv theorem

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

Full source

@[simp]
theorem pointReflection_toAffineEquiv (x : P) :
    (pointReflection 𝕜 x).toAffineEquiv = AffineEquiv.pointReflection 𝕜 x :=
  rfl

Point Reflection's Underlying Affine Equivalence

Informal description

For any point $x$ in an affine space $P$ over a normed field $\mathbb{K}$, the underlying affine equivalence of the point reflection isometric automorphism about $x$ is equal to the affine equivalence given by point reflection about $x$. That is, $\text{toAffineEquiv}(\text{pointReflection}_{\mathbb{K}}(x)) = \text{AffineEquiv.pointReflection}_{\mathbb{K}}(x)$.

AffineIsometryEquiv.pointReflection_self theorem

(x : P) : pointReflection 𝕜 x x = x

Full source

@[simp]
theorem pointReflection_self (x : P) : pointReflection 𝕜 x x = x :=
  AffineEquiv.pointReflection_self 𝕜 x

Fixed Point Property of Point Reflection

Informal description

For any point $x$ in an affine space $P$ over a normed field $\mathbb{K}$, the point reflection about $x$ maps $x$ to itself, i.e., $\text{pointReflection}_{\mathbb{K}}(x)(x) = x$.

AffineIsometryEquiv.pointReflection_involutive theorem

(x : P) : Function.Involutive (pointReflection 𝕜 x)

Full source

theorem pointReflection_involutive (x : P) : Function.Involutive (pointReflection 𝕜 x) :=
  Equiv.pointReflection_involutive x

Involutivity of Point Reflection in Affine Space

Informal description

For any point $x$ in an affine space $P$ over a normed field $\mathbb{K}$, the point reflection map about $x$ is involutive, i.e., applying the reflection twice returns the original point: $\text{pointReflection}_{\mathbb{K}}(x) \circ \text{pointReflection}_{\mathbb{K}}(x) = \text{id}_P$.

AffineIsometryEquiv.pointReflection_symm theorem

(x : P) : (pointReflection 𝕜 x).symm = pointReflection 𝕜 x

Full source

@[simp]
theorem pointReflection_symm (x : P) : (pointReflection 𝕜 x).symm = pointReflection 𝕜 x :=
  toAffineEquiv_injective <| AffineEquiv.pointReflection_symm 𝕜 x

Point Reflection is Self-Inverse

Informal description

For any point $x$ in an affine space $P$ over a normed field $\mathbb{K}$, the inverse of the point reflection about $x$ is equal to the point reflection about $x$ itself, i.e., $(\text{pointReflection}_{\mathbb{K}} x)^{-1} = \text{pointReflection}_{\mathbb{K}} x$.

AffineIsometryEquiv.dist_pointReflection_fixed theorem

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

Full source

@[simp]
theorem dist_pointReflection_fixed (x y : P) : dist (pointReflection 𝕜 x y) x = dist y x := by
  rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]

Distance Preservation Under Point Reflection: $\operatorname{dist}(f_x(y), x) = \operatorname{dist}(y, x)$

Informal description

For any points $x$ and $y$ in an affine space $P$ over a normed field $\mathbb{K}$, the distance between the point reflection of $y$ about $x$ and $x$ itself is equal to the distance between $y$ and $x$, i.e., $\operatorname{dist}(\text{pointReflection}_{\mathbb{K}}(x)(y), x) = \operatorname{dist}(y, x)$.

AffineIsometryEquiv.dist_pointReflection_self' theorem

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

Full source

theorem dist_pointReflection_self' (x y : P) :
    dist (pointReflection 𝕜 x y) y = ‖2 • (x -ᵥ y)‖ := by
  rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, two_nsmul]

Distance Formula for Point Reflection: $\text{dist}(f_x(y), y) = \|2(x-y)\|$

Informal description

For any points $x$ and $y$ in an affine space $P$ over a normed field $\mathbb{K}$, the distance between the point reflection of $y$ about $x$ and $y$ itself is equal to the norm of twice the vector from $y$ to $x$, i.e., $\text{dist}(\text{pointReflection}_{\mathbb{K}}(x)(y), y) = \|2 \cdot (x - y)\|$.

AffineIsometryEquiv.dist_pointReflection_self theorem

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

Full source

theorem dist_pointReflection_self (x y : P) :
    dist (pointReflection 𝕜 x y) y = ‖(2 : 𝕜)‖ * dist x y := by
  rw [dist_pointReflection_self', two_nsmul, ← two_smul 𝕜, norm_smul, ← dist_eq_norm_vsub V]

Distance Formula for Point Reflection: $\text{dist}(f_x(y), y) = \|2\| \cdot \text{dist}(x, y)$

Informal description

For any points $x$ and $y$ in an affine space $P$ over a normed field $\mathbb{K}$, the distance between the point reflection of $y$ about $x$ and $y$ itself is equal to the norm of $2$ in $\mathbb{K}$ multiplied by the distance between $x$ and $y$, i.e., $\text{dist}(\text{pointReflection}_{\mathbb{K}}(x)(y), y) = \|2\|_{\mathbb{K}} \cdot \text{dist}(x, y)$.

AffineIsometryEquiv.pointReflection_fixed_iff theorem

[Invertible (2 : 𝕜)] {x y : P} : pointReflection 𝕜 x y = y ↔ y = x

Full source

theorem pointReflection_fixed_iff [Invertible (2 : 𝕜)] {x y : P} :
    pointReflectionpointReflection 𝕜 x y = y ↔ y = x :=
  AffineEquiv.pointReflection_fixed_iff_of_module 𝕜

Fixed Point Condition for Affine Point Reflection

Informal description

Let $\mathbb{K}$ be a normed field where $2$ is invertible, and let $P$ be a normed affine space over $\mathbb{K}$. For any points $x, y \in P$, the point reflection of $y$ about $x$ equals $y$ if and only if $y = x$.

AffineIsometryEquiv.dist_pointReflection_self_real theorem

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

Full source

theorem dist_pointReflection_self_real (x y : P) :
    dist (pointReflection ℝ x y) y = 2 * dist x y := by
  rw [dist_pointReflection_self, Real.norm_two]

Distance Formula for Real Point Reflection: $\text{dist}(f_x(y), y) = 2 \cdot \text{dist}(x, y)$

Informal description

For any points $x$ and $y$ in a real normed affine space $P$, the distance between the point reflection of $y$ about $x$ and $y$ itself is equal to twice the distance between $x$ and $y$, i.e., $\text{dist}(\text{pointReflection}_{\mathbb{R}}(x)(y), y) = 2 \cdot \text{dist}(x, y)$.

AffineIsometryEquiv.pointReflection_midpoint_left theorem

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

Full source

@[simp]
theorem pointReflection_midpoint_left (x y : P) : pointReflection ℝ (midpoint ℝ x y) x = y :=
  AffineEquiv.pointReflection_midpoint_left x y

Point Reflection of First Point About Midpoint Equals Second Point in Real Affine Space

Informal description

For any two points $x$ and $y$ in a real normed affine space $P$, the point reflection of $x$ about their midpoint equals $y$. That is, if $m$ is the midpoint of $x$ and $y$, then the point reflection $\phi_m(x) = y$, where $\phi_m$ denotes the reflection map centered at $m$.

AffineIsometryEquiv.pointReflection_midpoint_right theorem

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

Full source

@[simp]
theorem pointReflection_midpoint_right (x y : P) : pointReflection ℝ (midpoint ℝ x y) y = x :=
  AffineEquiv.pointReflection_midpoint_right x y

Point reflection of $y$ about midpoint of $x$ and $y$ equals $x$

Informal description

For any two points $x$ and $y$ in an affine space $P$ over $\mathbb{R}$, the point reflection of $y$ about the midpoint of $x$ and $y$ equals $x$. That is, if $m$ is the midpoint of $x$ and $y$, then the point reflection $\text{pointReflection}_{\mathbb{R}}(m, y) = x$.

AffineMap.continuous_linear_iff theorem

{f : P →ᵃ[𝕜] P₂} : Continuous f.linear ↔ Continuous f

Full source

/-- If `f` is an affine map, then its linear part is continuous iff `f` is continuous. -/
theorem AffineMap.continuous_linear_iff {f : P →ᵃ[𝕜] P₂} : ContinuousContinuous f.linear ↔ Continuous f := by
  inhabit P
  have :
    (f.linear : V → V₂) =
      (AffineIsometryEquiv.vaddConst 𝕜 <| f default).toHomeomorph.symm ∘
        f ∘ (AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph := by
    ext v
    simp
  rw [this]
  simp only [Homeomorph.comp_continuous_iff, Homeomorph.comp_continuous_iff']

Continuity of Affine Map Equivalent to Continuity of its Linear Part

Informal description

For an affine map $f \colon P \to P₂$ between normed affine spaces over a normed field $\mathbb{K}$, the linear part of $f$ is continuous if and only if $f$ itself is continuous.

AffineMap.isOpenMap_linear_iff theorem

{f : P →ᵃ[𝕜] P₂} : IsOpenMap f.linear ↔ IsOpenMap f

Full source

/-- If `f` is an affine map, then its linear part is an open map iff `f` is an open map. -/
theorem AffineMap.isOpenMap_linear_iff {f : P →ᵃ[𝕜] P₂} : IsOpenMapIsOpenMap f.linear ↔ IsOpenMap f := by
  inhabit P
  have :
    (f.linear : V → V₂) =
      (AffineIsometryEquiv.vaddConst 𝕜 <| f default).toHomeomorph.symm ∘
        f ∘ (AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph := by
    ext v
    simp
  rw [this]
  simp only [Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff']

Affine map is open if and only if its linear part is open

Informal description

For an affine map $f \colon P \to P₂$ over a normed field $\mathbb{K}$, the linear part of $f$ is an open map if and only if $f$ itself is an open map.

AffineSubspace.equivMapOfInjective definition

 (E : AffineSubspace 𝕜 P₁) [Nonempty E] (φ : P₁ →ᵃ[𝕜] P₂) (hφ : Function.Injective φ) : E ≃ᵃ[𝕜] E.map φ

Full source

/-- An affine subspace is isomorphic to its image under an injective affine map.
This is the affine version of `Submodule.equivMapOfInjective`.
-/
@[simps linear, simps! toFun]
noncomputable def equivMapOfInjective (E : AffineSubspace 𝕜 P₁) [Nonempty E] (φ : P₁ →ᵃ[𝕜] P₂)
    (hφ : Function.Injective φ) : E ≃ᵃ[𝕜] E.map φ :=
  { Equiv.Set.image _ (E : Set P₁) hφ with
    linear :=
      (E.direction.equivMapOfInjective φ.linear (φ.linear_injective_iff.mpr hφ)).trans
        (LinearEquiv.ofEq _ _ (AffineSubspace.map_direction _ _).symm)
    map_vadd' := fun p v => Subtype.ext <| φ.map_vadd p v }

Affine equivalence between a subspace and its image under an injective affine map

Informal description

Given an affine subspace $ E $ of $ P_1 $ (with a nonempty carrier) and an injective affine map $ \phi : P_1 \to P_2 $, there exists an affine equivalence between $ E $ and its image under $ \phi $, denoted $ E.\text{map} \phi $. More precisely, the equivalence is constructed as follows: - The underlying set-theoretic bijection is given by the restriction of $ \phi $ to $ E $, which is a bijection onto its image due to injectivity. - The linear part of the equivalence is obtained by composing the linear equivalence induced by the injective linear map $ \phi.\text{linear} $ on the direction subspace of $ E $ with a linear equivalence that adjusts for the direction of the mapped subspace.

AffineSubspace.isometryEquivMap definition

(φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁') [Nonempty E] : E ≃ᵃⁱ[𝕜] E.map φ.toAffineMap

Full source

/-- 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.
-/
noncomputable def isometryEquivMap (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁') [Nonempty E] :
    E ≃ᵃⁱ[𝕜] E.map φ.toAffineMap :=
  ⟨E.equivMapOfInjective φ.toAffineMap φ.injective, fun _ => φ.norm_map _⟩

Affine isometric equivalence between a subspace and its image under an affine isometry

Informal description

Given an affine isometry $\phi \colon P_1' \to P_2$ and a nonempty affine subspace $E$ of $P_1'$, the function constructs an affine isometric equivalence between $E$ and its image under $\phi$. More precisely, the equivalence is given by restricting $\phi$ to $E$, which is bijective onto its image (since $\phi$ is injective), and preserves distances (since $\phi$ is an isometry).

AffineSubspace.isometryEquivMap.apply_symm_apply theorem

 {E : AffineSubspace 𝕜 P₁'} [Nonempty E] {φ : P₁' →ᵃⁱ[𝕜] P₂} (x : E.map φ.toAffineMap) :
  φ ((E.isometryEquivMap φ).symm x) = x

Full source

@[simp]
theorem isometryEquivMap.apply_symm_apply {E : AffineSubspace 𝕜 P₁'} [Nonempty E]
    {φ : P₁' →ᵃⁱ[𝕜] P₂} (x : E.map φ.toAffineMap) : φ ((E.isometryEquivMap φ).symm x) = x :=
  congr_arg Subtype.val <| (E.isometryEquivMap φ).apply_symm_apply _

Affine Isometric Equivalence Preserves Inverse Image: $\phi(\psi^{-1}(x)) = x$ for $\psi \colon E \simeq^{ai}[\mathbb{K}] \phi(E)$

Informal description

Let $E$ be a nonempty affine subspace of a normed affine space $P_1'$ over a normed field $\mathbb{K}$, and let $\phi \colon P_1' \to P_2$ be an affine isometry. For any point $x$ in the image of $E$ under $\phi$, applying $\phi$ to the inverse image of $x$ under the affine isometric equivalence $E \simeq^{ai}[\mathbb{K}] \phi(E)$ yields $x$ itself, i.e., $\phi((E \simeq^{ai}[\mathbb{K}] \phi(E))^{-1}(x)) = x$.

AffineSubspace.isometryEquivMap.coe_apply theorem

 (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁') [Nonempty E] (g : E) : ↑(E.isometryEquivMap φ g) = φ g

Full source

@[simp]
theorem isometryEquivMap.coe_apply (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁') [Nonempty E]
    (g : E) : ↑(E.isometryEquivMap φ g) = φ g :=
  rfl

Image of Subspace Element under Affine Isometric Equivalence

Informal description

Let $\phi \colon P_1' \to P_2$ be an affine isometry, $E$ be a nonempty affine subspace of $P_1'$, and $g$ be an element of $E$. Then the image of $g$ under the affine isometric equivalence $E \simeq^{ai}[\mathbb{K}] \phi(E)$ (obtained by restricting $\phi$ to $E$) equals $\phi(g)$ when viewed as an element of $P_2$.

AffineSubspace.isometryEquivMap.toAffineMap_eq theorem

 (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁') [Nonempty E] :
  (E.isometryEquivMap φ).toAffineMap = E.equivMapOfInjective φ.toAffineMap φ.injective

Full source

@[simp]
theorem isometryEquivMap.toAffineMap_eq (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁')
    [Nonempty E] :
    (E.isometryEquivMap φ).toAffineMap = E.equivMapOfInjective φ.toAffineMap φ.injective :=
  rfl

Equality of Affine Maps in Isometric Subspace Equivalence

Informal description

Let $\phi \colon P_1' \to P_2$ be an affine isometry and $E$ be a nonempty affine subspace of $P_1'$. Then the underlying affine map of the isometric equivalence $E \simeq^{a\mathbb{K}} E.\text{map} \phi$ (constructed via `isometryEquivMap`) is equal to the affine equivalence $E \simeq^{a\mathbb{K}} E.\text{map} \phi$ obtained by restricting $\phi$ to $E$ (constructed via `equivMapOfInjective`).

Notation