isCompactOperator_iff_isCompact_closure_image_ball

English

If f is compact, then there exists a neighborhood V of 0 such that f(V) has compact closure, and conversely.

Русский

У компактности f существуют окрестность V(0) так, что образ f(V) имеет компактное замыкание, и наоборот.

LaTeX

$$$IsCompactOperator(f) \iff \exists V \in 𝓝(0), IsCompact( closure( f'' V) )$$$

Lean4

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

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