Theorems · Definition · functional analysis

LinearIsometry.toLinearIsometryEquiv

{F : Type u_1} →
  {E₁ : Type u_2} →
    [inst : SeminormedAddCommGroup F] →
      [inst_1 : NormedAddCommGroup E₁] →
        {R₁ : Type u_3} →
          [inst_2 : Field R₁] →
            [inst_3 : Module R₁ E₁] →
              [inst_4 : Module R₁ F] →
                [FiniteDimensional R₁ E₁] →
                  [FiniteDimensional R₁ F] → (E₁ →ₗᵢ[R₁] F) → Module.finrank R₁ E₁ = Module.finrank R₁ F → E₁ ≃ₗᵢ[R₁] F

A linear isometry between finite-dimensional spaces of equal dimension can be upgraded to a linear isometry equivalence.

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

4 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedAddCommGroupFieldModuleModuleFiniteDimensionalFiniteDimensional