Theorems · Definition · functional analysis

LinearIsometry.extend

{𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {V : Type u_7} →
      [inst_1 : NormedAddCommGroup V] →
        [inst_2 : InnerProductSpace 𝕜 V] → [FiniteDimensional 𝕜 V] → {S : Submodule 𝕜 V} → (↥S →ₗᵢ[𝕜] V) → V →ₗᵢ[𝕜] V

Let S be a subspace of a finite-dimensional complex inner product space V. A linear isometry mapping S into V can be extended to a full isometry of V. TODO: The case when S is a finite-dimensional subspace of an infinite-dimensional V.

Defined in

Mathlib.Analysis.InnerProductSpace.PiL2

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensional