image_ball_subset_compact — Mathlib

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)

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