Theorems · Theorem · operator theory

isCompactOperator_of_tendsto

∀ {ι : Type u_1} {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_4} {M₂ : Type u_5} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : AddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜₁ M₁] [inst_5 : Module 𝕜₂ M₂] [inst_6 : UniformSpace M₂] [inst_7 : IsUniformAddGroup M₂]
  [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂] {l : Filter ι} [l.NeBot] {F : ι → M₁ →SL[σ₁₂] M₂}
  {f : M₁ →SL[σ₁₂] M₂}, Filter.Tendsto F l (nhds f) → (∀ᶠ (i : ι) in l, IsCompactOperator ⇑(F i)) → IsCompactOperator ⇑f

Defined in

Mathlib.Analysis.Normed.Operator.Compact.Basic

Cited by

0 results in Mathlib

Foundations

Depth 128 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedFieldSeminormedAddCommGroupAddCommGroupNormedSpaceModuleUniformSpaceIsUniformAddGroupContinuousConstSMulT2SpaceCompleteSpaceFilter.NeBot