∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_3} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] {f : M₁ →ₗ[R₁] M₁},
  IsCompactOperator ⇑f →
    ∀ {V : Submodule R₁ M₁} (hV : ∀ v ∈ V, f v ∈ V), IsClosed ↑V → IsCompactOperator ⇑(f.restrict hV)