isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image

English

For a map f: M1 → M2, f is compact iff there exists a neighborhood V of 0 in M1 such that the closure of the image f[V] is compact.

Русский

Для отображения f: M1 → M2 лемма: компактность эквивалентна существованию окрестности V точки 0 в M1 such that замыкание образа f[V] компактно.

LaTeX

$$$IsCompactOperator(f) \iff \exists V \in (\mathcal{N}(0) : Filter M_1), IsCompact(\overline{f''V})$$$

Lean4

theorem isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image [T2Space M₂] (f : M₁ → M₂) :
    IsCompactOperator f ↔ ∃ V ∈ (𝓝 0 : Filter M₁), IsCompact (closure <| f '' V) :=
  by
  rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]
  exact
    ⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, hK.closure_of_subset hKV⟩, fun ⟨V, hV, hVc⟩ =>
      ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩

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