isCompactOperator_iff_image_ball_subset_compact

English

For a compact operator f and any radius r, the image f(ball 0 r) is contained in some compact K.

Русский

Для компактного оператора f и любого радиуса сфера образ f(ball(0, r)) содержится внутри некоторого компактного K.

LaTeX

$$$IsCompactOperator(f) \Rightarrow \exists K(IsCompact(K) \land f'' ball(0,r) ⊆ K)$$$

Lean4

theorem isCompactOperator_iff_image_ball_subset_compact [ContinuousConstSMul 𝕜₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) {r : ℝ}
    (hr : 0 < r) : IsCompactOperator f ↔ ∃ K : Set M₂, IsCompact K ∧ f '' Metric.ball 0 r ⊆ K :=
  ⟨fun hf => hf.image_ball_subset_compact r, fun ⟨K, hK, hKr⟩ =>
    (isCompactOperator_iff_exists_mem_nhds_image_subset_compact f).mpr
      ⟨Metric.ball 0 r, ball_mem_nhds _ hr, K, hK, hKr⟩⟩

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