English
If f is a compact operator, then for any bounded set S, the image f[S] is contained in some compact K.
Русский
Если f компактный оператор, то образ любого ограниченного множества S лежит внутри некоторого компактного множества K.
LaTeX
$$$IsCompactOperator(f) \Rightarrow \forall S, IsBounded(S) \Rightarrow \exists K, IsCompact(K) \land f''S ⊆ K$$$
Lean4
theorem image_ball_subset_compact [ContinuousConstSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) (r : ℝ) :
∃ K : Set M₂, IsCompact K ∧ f '' Metric.ball 0 r ⊆ K :=
hf.image_subset_compact_of_isVonNBounded (NormedSpace.isVonNBounded_ball 𝕜₁ M₁ r)