Theorems · Definition · functional analysis

IsometryEquiv.toRealLinearIsometryEquivOfMapZero

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

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.

Defined in

Mathlib.Analysis.Normed.Affine.MazurUlam

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace