isCompact_closure_image_ball — Mathlib

English

If f is compact operator, then for a Von Neumann bounded S, f[S] has compact closure.

Русский

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

LaTeX

$$$IsCompactOperator(f) \Rightarrow IsCompact(closure(f''S)) \\text{ forVonNBounded } S$$$

Lean4

theorem isCompact_closure_image_ball [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}
    (hf : IsCompactOperator f) (r : ℝ) : IsCompact (closure <| f '' Metric.ball 0 r) :=
  hf.isCompact_closure_image_of_isVonNBounded (NormedSpace.isVonNBounded_ball 𝕜₁ M₁ r)

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