image_closedBall_subset_compact — Mathlib

English

The compactness of a linear map f can be characterized by the property that for any bounded set S, the image f[S] lies within some compact set.

Русский

Компактность линейного отображения можно охарактеризовать так: для любого ограниченного множества S образ f[S] лежит в компактном множестве.

LaTeX

$$$\text{IsCompactOperator}(f) \iff \forall S (IsBounded(S) \Rightarrow \exists K(IsCompact(K) \land f''S ⊆ K))$$$

Lean4

theorem image_closedBall_subset_compact [ContinuousConstSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f)
    (r : ℝ) : ∃ K : Set M₂, IsCompact K ∧ f '' Metric.closedBall 0 r ⊆ K :=
  hf.image_subset_compact_of_isVonNBounded (NormedSpace.isVonNBounded_closedBall 𝕜₁ M₁ r)

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