isCompactOperator_iff_isCompact_closure_image_closedBall

English

If f is compact and r > 0, then the closure of the image of the closed ball of radius r is compact.

Русский

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

LaTeX

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

Lean4

theorem isCompactOperator_iff_isCompact_closure_image_closedBall [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂]
    (f : M₁ →ₛₗ[σ₁₂] M₂) {r : ℝ} (hr : 0 < r) :
    IsCompactOperator f ↔ IsCompact (closure <| f '' Metric.closedBall 0 r) :=
  ⟨fun hf => hf.isCompact_closure_image_closedBall r, fun hf =>
    (isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image f).mpr
      ⟨Metric.closedBall 0 r, closedBall_mem_nhds _ hr, hf⟩⟩

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