English
If a net of compact operators tends to f, then f is compact.
Русский
Если сетка компактных операторов слабо сходится к f, то f — компактный.
LaTeX
$$$\\text{Tendsto } F\\ l\\to f \\Rightarrow (\\forall i, IsCompactOperator(F_i)) \\Rightarrow IsCompactOperator f$$$
Lean4
theorem isCompactOperator_of_tendsto {ι 𝕜₁ 𝕜₂ : Type*} [NontriviallyNormedField 𝕜₁] [NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ M₂ : Type*} [SeminormedAddCommGroup M₁] [AddCommGroup M₂] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [UniformSpace M₂]
[IsUniformAddGroup M₂] [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂] {l : Filter ι} [l.NeBot]
{F : ι → M₁ →SL[σ₁₂] M₂} {f : M₁ →SL[σ₁₂] M₂} (hf : Tendsto F l (𝓝 f)) (hF : ∀ᶠ i in l, IsCompactOperator (F i)) :
IsCompactOperator f :=
isClosed_setOf_isCompactOperator.mem_of_tendsto hf hF
