toRealLinearIsometryEquiv — Mathlib

English

For an affine subspace E and an isometry φ, the associated isometryEquivMap aligns with the intrinsic affine map of φ on E.

Русский

Для аффинного подпространства E и изометрии φ соответствующее isometryEquivMap совпадает с внутренним аффинным отображением φ на E.

LaTeX

$$$(E.isometryEquivMap\phi).toAffineMap = E.equivMapOfInjective(\phi.toAffineMap, \phi.injective)$$$

Lean4

/-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed vector spaces
over `ℝ`, then `x ↦ f x - f 0` is a linear isometry equivalence. -/
def toRealLinearIsometryEquiv (f : E ≃ᵢ F) : E ≃ₗᵢ[ℝ] F :=
  (f.trans (IsometryEquiv.addRight (f 0)).symm).toRealLinearIsometryEquivOfMapZero
    (by simpa only [sub_eq_add_neg] using sub_self (f 0))

Похожие утверждения