isCompact_image_coe_of_bounded_of_closed_image

English

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

Русский

Замыкание множества компактных операторов равно самому множеству.

LaTeX

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

Lean4

/-- Let `s` be a bounded set in the space of continuous (semi)linear maps `E →SL[σ] F` taking values
in a proper space. If `s` interpreted as a set in the space of maps `E → F` with topology of
pointwise convergence is closed, then it is compact.

TODO: reformulate this in terms of a type synonym with the right topology. -/
theorem isCompact_image_coe_of_bounded_of_closed_image [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : IsBounded s)
    (hc : IsClosed (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s)) : IsCompact (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s) :=
  hc.closure_eq ▸ isCompact_closure_image_coe_of_bounded hb

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