comp_clm — Mathlib

English

If f is compact and is subjected to a base change (in a categorical sense), the resulting operator remains compact.

Русский

Если f компактный и применяется базовый переход, получившийся оператор остаётся компактным.

LaTeX

$$$IsCompactOperator(f) \Rightarrow IsCompactOperator(g \circ f)$$ for suitable g$$

Lean4

theorem comp_clm [AddCommMonoid M₂] [Module R₂ M₂] {f : M₂ → M₃} (hf : IsCompactOperator f) (g : M₁ →SL[σ₁₂] M₂) :
    IsCompactOperator (f ∘ g) := by
  have := g.continuous.tendsto 0
  rw [map_zero] at this
  rcases hf with ⟨K, hK, hKf⟩
  exact ⟨K, hK, this hKf⟩

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