Theorems · Definition · functional analysis

LinearMap.extendOfNorm

{𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {Eₗ : Type u_4} →
        {F : Type u_5} →
          [inst : NormedDivisionRing 𝕜] →
            [inst_1 : NormedDivisionRing 𝕜₂] →
              {σ₁₂ : 𝕜 →+* 𝕜₂} →
                [inst_2 : AddCommGroup E] →
                  [inst_3 : SeminormedAddCommGroup Eₗ] →
                    [inst_4 : NormedAddCommGroup F] →
                      [inst_5 : Module 𝕜 E] →
                        [inst_6 : Module 𝕜₂ F] →
                          [IsBoundedSMul 𝕜₂ F] →
                            [inst_8 : Module 𝕜 Eₗ] →
                              [IsBoundedSMul 𝕜 Eₗ] → [CompleteSpace F] → (E →ₛₗ[σ₁₂] F) → (E →ₗ[𝕜] Eₗ) → Eₗ →SL[σ₁₂] F

Extension of a linear map f : E →ₛₗ[σ₁₂] F to a continuous linear map Eₗ →SL[σ₁₂] F, where E is a normed space and F a complete normed space, using a dense map e : E →ₗ[𝕜] Eₗ together with a bound ‖f x‖ ≤ C * ‖e x‖ for all x : E.

Defined in

Mathlib.Analysis.Normed.Operator.Extend

Cited by

9 results in Mathlib

Foundations

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

Assumes

NormedDivisionRingNormedDivisionRingAddCommGroupSeminormedAddCommGroupNormedAddCommGroupModuleModuleIsBoundedSMulModuleIsBoundedSMulCompleteSpace