compactOperator_topologicalClosure

English

The topological closure of the set of compact operators equals the set itself.

Русский

Топологическое замыкание множества компактных операторов равно самому множеству.

LaTeX

$$$ (\\mathrm{compactOperator}\\;\\sigma_{12}\\;M_1\\;M_2).\\mathrm{topologicalClosure} = \\mathrm{compactOperator}\\;\\sigma_{12}\\;M_1\\;M_2 $$$

Lean4

theorem compactOperator_topologicalClosure {𝕜₁ 𝕜₂ : Type*} [NontriviallyNormedField 𝕜₁] [NormedField 𝕜₂]
    {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ M₂ : Type*} [SeminormedAddCommGroup M₁] [AddCommGroup M₂] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂]
    [UniformSpace M₂] [IsUniformAddGroup M₂] [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂] :
    (compactOperator σ₁₂ M₁ M₂).topologicalClosure = compactOperator σ₁₂ M₁ M₂ :=
  SetLike.ext' isClosed_setOf_isCompactOperator.closure_eq

Похожие утверждения