isCompact_closure_image_coe_of_bounded

English

IsClosed of the set of compact operators.

Русский

IsClosed множества компактных операторов.

LaTeX

$$$\\mathrm{IsClosed}\\{ f : M_1 \\toSL[\\sigma_{12}] M_2 \\mid \\mathrm{IsCompactOperator}(f) \\}$$$

Lean4

/-- Let `s` be a bounded set in the space of continuous (semi)linear maps `E →SL[σ] F` taking values
in a proper space. Then `s` interpreted as a set in the space of maps `E → F` with topology of
pointwise convergence is precompact: its closure is a compact set. -/
theorem isCompact_closure_image_coe_of_bounded [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : IsBounded s) :
    IsCompact (closure (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s)) :=
  have : ∀ x, IsCompact (closure (apply' F σ₁₂ x '' s)) := fun x =>
    ((apply' F σ₁₂ x).lipschitz.isBounded_image hb).isCompact_closure
  (isCompact_pi_infinite this).closure_of_subset
    (image_subset_iff.2 fun _ hg _ => subset_closure <| mem_image_of_mem _ hg)

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