isCompactOperator_iff_image_closedBall_subset_compact

English

If f is compact and g is a continuous linear map, then their composition g ∘ f is compact.

Русский

Если f компактный, а g — непрерывное линейное отображение, то композиция g ∘ f компактна.

LaTeX

$$$\text{IsCompactOperator}(f) \Rightarrow \text{IsCompactOperator}(g \circ f)$, where g is continuous linear$$

Lean4

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

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