English
If f is a compact operator, then its restriction to a suitable closed subspace is compact.
Русский
Если f компактный оператор, то его ограничение на подходящее замкнутое подпространство также компактно.
LaTeX
$$$IsCompactOperator(f) \Rightarrow IsCompactOperator(f|_V)$ for closed V$$
Lean4
/-- If a compact operator preserves a closed 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 {f : M₁ →ₗ[R₁] M₁} (hf : IsCompactOperator f) {V : Submodule R₁ M₁} (hV : ∀ v ∈ V, f v ∈ V)
(h_closed : IsClosed (V : Set M₁)) : IsCompactOperator (f.restrict hV) :=
(hf.comp_clm V.subtypeL).codRestrict (SetLike.forall.2 hV) h_closed
