image_subset_compact_of_bounded — Mathlib

English

If f is a compact operator and S is Von Neumann bounded, then the closure of the image f[S] is compact.

Русский

Если f компактный оператор и S Von Neumann ограничено, то замыкание образа f[S] компактно.

LaTeX

$$$IsCompact(f) \Rightarrow IsCompact(\overline{f''S})$ under appropriate hypotheses$$

Lean4

theorem image_subset_compact_of_bounded [ContinuousConstSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f)
    {S : Set M₁} (hS : Bornology.IsBounded S) : ∃ K : Set M₂, IsCompact K ∧ f '' S ⊆ K :=
  hf.image_subset_compact_of_isVonNBounded <| by rwa [NormedSpace.isVonNBounded_iff]

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