isCompact_closure_image_closedBall

English

For a compact operator f and radius r > 0, the closure of the image of the closed ball is compact.

Русский

Для компактного оператора f и радиуса r > 0 замыкание образа замкнутого шара является компактным.

LaTeX

$$$IsCompactOperator(f) \land r>0 \Rightarrow IsCompact(closure( f'' ball(0,r) ))$$$

Lean4

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

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