toRealLinearIsometryEquivOfMapZero

English

For any isometry f: E ≃ᵢ F, the associated real-affine isometry equivalence sends p to f p in a linear-affine fashion.

Русский

Для любой изометрии f: E ≃ᵢ F сопряженная реал-абсолютная аффинная изометрия переводит точку p в f(p) линейно-аффиновым образом.

LaTeX

$$$f: E\simeq_i F \Rightarrow f^{\text{toRealAffineIsometryEquiv}}: E\simeq_A^{\mathbb{R}} F$$$

Lean4

/-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed vector spaces
over `ℝ` and `f 0 = 0`, then `f` is a linear isometry equivalence. -/
def toRealLinearIsometryEquivOfMapZero (f : E ≃ᵢ F) (h0 : f 0 = 0) : E ≃ₗᵢ[ℝ] F :=
  { (AddMonoidHom.ofMapMidpoint ℝ ℝ f h0 f.map_midpoint).toRealLinearMap f.continuous, f with
    norm_map' := fun x => show ‖f x‖ = ‖x‖ by simp only [← dist_zero_right, ← h0, f.dist_eq] }

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