codRestrict — Mathlib

English

If f is a compact operator and V is a closed subspace with appropriate containment, then the codRestrict of f to V is compact.

Русский

Если f компактный оператор и V — замкнутое подпространство с нужными условиями, то codRestrict f к V остаётся компактным.

LaTeX

$$$IsCompactOperator(f) \Rightarrow IsCompactOperator(Set.codRestrict f V hV)$, при условии hV и закрытости$$

Lean4

theorem codRestrict {f : M₁ → M₂} (hf : IsCompactOperator f) {V : Submodule R₂ M₂} (hV : ∀ x, f x ∈ V)
    (h_closed : IsClosed (V : Set M₂)) : IsCompactOperator (Set.codRestrict f V hV) :=
  let ⟨_, hK, hKf⟩ := hf
  ⟨_, h_closed.isClosedEmbedding_subtypeVal.isCompact_preimage hK, hKf⟩

Похожие утверждения