Theorems · Theorem · operator theory

isClosed_setOf_isCompactOperator

Deprecated since 2026-07-09Use isClosed_setOfPred_isCompactOperator instead.

∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [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₂], IsClosed {f | IsCompactOperator ⇑f}

Alias of isClosed_setOfPred_isCompactOperator. The set of compact operators from a normed space to a complete topological vector space is closed.

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

NontriviallyNormedFieldNormedFieldSeminormedAddCommGroupAddCommGroupNormedSpaceModuleUniformSpaceIsUniformAddGroupContinuousConstSMulT2SpaceCompleteSpace