clm_comp — Mathlib

English

If f is compact and g is a continuous linear map, then the composition f ∘ g is compact.

Русский

Если f компактный и g — непрерывное линейное отображение, то композиция f ∘ g компактна.

LaTeX

$$$IsCompactOperator(f) \Rightarrow IsCompactOperator(\text{coeff}(g) \circ f)$$$

Lean4

theorem clm_comp [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid M₃] [Module R₃ M₃] {f : M₁ → M₂}
    (hf : IsCompactOperator f) (g : M₂ →SL[σ₂₃] M₃) : IsCompactOperator (g ∘ f) :=
  hf.continuous_comp g.continuous

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