Theorems · Definition · functional analysis

LinearEquiv.extendOfIsometry

{𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {Eₗ : Type u_4} →
        {F : Type u_5} →
          {Fₗ : Type u_6} →
            [inst : NormedField 𝕜] →
              [inst_1 : NormedField 𝕜₂] →
                [inst_2 : AddCommGroup E] →
                  [inst_3 : Module 𝕜 E] →
                    [inst_4 : AddCommGroup F] →
                      [inst_5 : Module 𝕜₂ F] →
                        [inst_6 : NormedAddCommGroup Eₗ] →
                          [inst_7 : NormedSpace 𝕜 Eₗ] →
                            [CompleteSpace Eₗ] →
                              [inst_9 : NormedAddCommGroup Fₗ] →
                                [inst_10 : NormedSpace 𝕜₂ Fₗ] →
                                  [CompleteSpace Fₗ] →
                                    {σ₁₂ : 𝕜 →+* 𝕜₂} →
                                      {σ₂₁ : 𝕜₂ →+* 𝕜} →
                                        [inst_12 : RingHomInvPair σ₁₂ σ₂₁] →
                                          [inst_13 : RingHomInvPair σ₂₁ σ₁₂] →
                                            (f : E ≃ₛₗ[σ₁₂] F) →
                                              (e₁ : E →ₗ[𝕜] Eₗ) →
                                                (e₂ : F →ₗ[𝕜₂] Fₗ) →
                                                  DenseRange ⇑e₁ →
                                                    DenseRange ⇑e₂ → (∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) → Eₗ ≃ₛₗᵢ[σ₁₂] Fₗ

Extend a densely defined operator that preserves the norm to a linear isometry equivalence.

Defined in

Mathlib.Analysis.Normed.Operator.Extend

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedFieldAddCommGroupModuleAddCommGroupModuleNormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceCompleteSpaceRingHomInvPairRingHomInvPair