compactOperator — Mathlib

English

A compact operator is a linear map whose image of the unit ball is relatively compact (i.e., the closure is compact).

Русский

Компактный оператор — линейное отображение, изображение единичного шара относительно компактно (замыкание образа компактно).

LaTeX

$$$IsCompactOperator(f) \equiv \text{(definition of compact operator in normed context)}$$$

Lean4

/-- The submodule of compact continuous linear maps. -/
def compactOperator [Module R₁ M₁] [Module R₄ M₄] [ContinuousConstSMul R₄ M₄] [IsTopologicalAddGroup M₄] :
    Submodule R₄ (M₁ →SL[σ₁₄] M₄) where
  carrier := {f | IsCompactOperator f}
  add_mem' hf hg := hf.add hg
  zero_mem' := isCompactOperator_zero
  smul_mem' c _ hf := hf.smul c

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