English
The set of compact operators is closed in the operator topology.
Русский
Множество компактных операторов является замкнутым в топологии операторов.
LaTeX
$$$\\mathrm{IsClosed}\\{ f : M_1 \\toSL[\\sigma_{12}] M_2 \\mid \\mathrm{IsCompactOperator}(f) \\}$$$
Lean4
/-- The set of compact operators from a normed space to a complete topological vector space is
closed. -/
theorem isClosed_setOf_isCompactOperator {𝕜₁ 𝕜₂ : Type*} [NontriviallyNormedField 𝕜₁] [NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ M₂ : Type*} [SeminormedAddCommGroup M₁] [AddCommGroup M₂] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [UniformSpace M₂]
[IsUniformAddGroup M₂] [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂] :
IsClosed {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator f} :=
by
refine isClosed_of_closure_subset ?_
rintro u hu
rw [mem_closure_iff_nhds_zero] at hu
suffices TotallyBounded (u '' Metric.closedBall 0 1)
by
change IsCompactOperator (u : M₁ →ₛₗ[σ₁₂] M₂)
rw [isCompactOperator_iff_isCompact_closure_image_closedBall (u : M₁ →ₛₗ[σ₁₂] M₂) zero_lt_one]
exact this.closure.isCompact_of_isClosed isClosed_closure
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]
intro U hU
rcases exists_nhds_zero_half hU with ⟨V, hV, hVU⟩
let SV : Set M₁ × Set M₂ := ⟨closedBall 0 1, -V⟩
rcases
hu {f | ∀ x ∈ SV.1, f x ∈ SV.2}
(ContinuousLinearMap.hasBasis_nhds_zero.mem_of_mem
⟨NormedSpace.isVonNBounded_closedBall _ _ _, neg_mem_nhds_zero M₂ hV⟩) with
⟨v, hv, huv⟩
rcases
totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp (hv.isCompact_closure_image_closedBall 1).totallyBounded V
hV with
⟨T, hT, hTv⟩
have hTv : v '' closedBall 0 1 ⊆ _ := subset_closure.trans hTv
refine ⟨T, hT, ?_⟩
rw [image_subset_iff, preimage_iUnion₂] at hTv ⊢
intro x hx
specialize hTv hx
rw [mem_iUnion₂] at hTv ⊢
rcases hTv with ⟨t, ht, htx⟩
refine ⟨t, ht, ?_⟩
rw [mem_preimage, mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, neg_add_eq_sub] at htx ⊢
convert hVU _ htx _ (huv x hx) using 1
rw [ContinuousLinearMap.sub_apply]
abel
