Theorems · Definition · operator theory

ContinuousLinearMap.mkOfIsCompactOperator

{𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NontriviallyNormedField 𝕜₁] →
      [inst_1 : NontriviallyNormedField 𝕜₂] →
        {σ₁₂ : 𝕜₁ →+* 𝕜₂} →
          [RingHomIsometric σ₁₂] →
            {M₁ : Type u_3} →
              {M₂ : Type u_4} →
                [inst_3 : TopologicalSpace M₁] →
                  [inst_4 : AddCommGroup M₁] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : AddCommGroup M₂] →
                        [inst_7 : Module 𝕜₁ M₁] →
                          [inst_8 : Module 𝕜₂ M₂] →
                            [IsTopologicalAddGroup M₁] →
                              [ContinuousConstSMul 𝕜₁ M₁] →
                                [IsTopologicalAddGroup M₂] →
                                  [ContinuousSMul 𝕜₂ M₂] → {f : M₁ →ₛₗ[σ₁₂] M₂} → IsCompactOperator ⇑f → M₁ →SL[σ₁₂] M₂

Upgrade a compact LinearMap to a ContinuousLinearMap.

Defined in

Mathlib.Analysis.Normed.Operator.Compact.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldRingHomIsometricTopologicalSpaceAddCommGroupTopologicalSpaceAddCommGroupModuleModuleIsTopologicalAddGroupContinuousConstSMulIsTopologicalAddGroupContinuousSMul