isCompactOperator_iff_exists_mem_nhds_image_subset_compact

English

A linear operator f is compact if and only if there exists a neighborhood V of 0 in the domain and a compact set K in the codomain such that the image f[V] is contained in K.

Русский

Линейный оператор f компактен тогда и только тогда, когда существует окрестность V точки 0 в области определения и компактное множество K в области значения such that f[V] ⊆ K.

LaTeX

$$$\text{IsCompactOperator}(f) \iff \exists V \in \mathcal{N}(0), \exists K\subseteq M_2, \ IsCompact(K) \land f[V] \subseteq K$$$

Lean4

theorem isCompactOperator_iff_exists_mem_nhds_image_subset_compact (f : M₁ → M₂) :
    IsCompactOperator f ↔ ∃ V ∈ (𝓝 0 : Filter M₁), ∃ K : Set M₂, IsCompact K ∧ f '' V ⊆ K :=
  ⟨fun ⟨K, hK, hKf⟩ => ⟨f ⁻¹' K, hKf, K, hK, image_preimage_subset _ _⟩, fun ⟨_, hV, K, hK, hVK⟩ =>
    ⟨K, hK, mem_of_superset hV (image_subset_iff.mp hVK)⟩⟩

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