mkOfIsCompactOperator_mem_compactOperator

English

The limit of a net of compact operators is compact.

Русский

Предел сечения компактных операторов остаётся компактным.

LaTeX

$$$\\text{If } (F_i) \\text{ are compact operators and } F_i \\to f, \\text{ then } f \\text{ is compact.}$$$

Lean4

theorem mkOfIsCompactOperator_mem_compactOperator {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) :
    ContinuousLinearMap.mkOfIsCompactOperator hf ∈ compactOperator σ₁₂ M₁ M₂ :=
  hf

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