English
Let f: P → P2 be an isometry between affine spaces, and for a base point p ∈ P define g: V → V2 by g(v) = f(v +ᵥ p) −ᵥ f(p). Then g is an isometry from V to V2.
Русский
Пусть f: P → P2 — изометрия между аффинными пространствами, и для базовой точки p ∈ P определить g: V → V2 по формуле g(v) = f(v +ᵥ p) −ᵥ f(p). Тогда g — изометрия между V и V2.
LaTeX
$$$\text{Isometry}(g)\quad\text{where } g(v) = f(v +_p) - f(p)\text{ for all } v\in V$$$
Lean4
/-- 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
