continuous_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem continuous_comp {f : M₁ → M₂} (hf : IsCompactOperator f) {g : M₂ → M₃} (hg : Continuous g) :
    IsCompactOperator (g ∘ f) := by
  rcases hf with ⟨K, hK, hKf⟩
  refine ⟨g '' K, hK.image hg, mem_of_superset hKf ?_⟩
  rw [preimage_comp]
  exact preimage_mono (subset_preimage_image _ _)

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