English
The coercion of a linear isometry equivalence to its affine isometry counterpart coincides with the original linear map when viewed as an affine map.
Русский
Коэрция линейной изометрической эквивалентности к соответствующей ей аффинной изометрии совпадает с исходной линейной картой, когда она рассматривается как аффинная карта.
LaTeX
$$$$ \uparrow\bigl( e.\mathrm{toAffineIsometryEquiv} \bigr) = e. $$$$
Lean4
/-- 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 }
