English
Let f be a compact linear operator on M₂ and let V be a complete subspace of M₂ such that f maps V into V. Then the restriction of f to V is compact.
Русский
Пусть f — компактный линейный оператор на M₂, и пусть V ⊆ M₂ — полное подпространство такое, что f(V) ⊆ V. Тогда ограничение f на V является компактным.
LaTeX
$$$\\text{IsCompactOperator}(f) \\;\\Rightarrow\\; \\forall V \\le M_2,\\ (\\forall v\\in V, f(v)\\in V) \\;\\land\\; \\text{CompleteSpace}(V) \\Rightarrow \\ IsCompactOperator(f\\restrict hV).$$$
Lean4
/-- If a compact operator preserves a complete submodule, its restriction to that submodule is
compact.
Note that, following mathlib's convention in linear algebra, `restrict` designates the restriction
of an endomorphism `f : E →ₗ E` to an endomorphism `f' : ↥V →ₗ ↥V`. To prove that the restriction
`f' : ↥U →ₛₗ ↥V` of a compact operator `f : E →ₛₗ F` is compact, apply
`IsCompactOperator.codRestrict` to `f ∘ U.subtypeL`, which is compact by
`IsCompactOperator.comp_clm`. -/
theorem restrict' [T0Space M₂] {f : M₂ →ₗ[R₂] M₂} (hf : IsCompactOperator f) {V : Submodule R₂ M₂}
(hV : ∀ v ∈ V, f v ∈ V) [hcomplete : CompleteSpace V] : IsCompactOperator (f.restrict hV) :=
hf.restrict hV (completeSpace_coe_iff_isComplete.mp hcomplete).isClosed
