Theorems · Definition · functional analysis

IsometryEquiv.toRealLinearIsometryEquiv

{E : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] → [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → E ≃ᵢ F → E ≃ₗᵢ[ℝ] F

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.

Defined in

Mathlib.Analysis.Normed.Affine.MazurUlam

Cited by

2 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace