isCompact_closure_image_of_bounded

English

For a compact operator f: M1 → M2, and S Von Neumann bounded, the closure of the image f[S] is compact.

Русский

Для компактного оператора f: M1 → M2 и Von Neumann ограниченного множества S замыкание образа f[S] компактно.

LaTeX

$$$IsCompactOperator(f) \land IsVonNBounded 𝕜 f \Rightarrow IsCompact(closure(f''S))$$$

Lean4

theorem isCompact_closure_image_of_bounded [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}
    (hf : IsCompactOperator f) {S : Set M₁} (hS : Bornology.IsBounded S) : IsCompact (closure <| f '' S) :=
  hf.isCompact_closure_image_of_isVonNBounded <| by rwa [NormedSpace.isVonNBounded_iff]

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