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