isCompact_closure_image_of_isVonNBounded

English

For a linear operator f: M1 → M2, IsCompactOperator f is equivalent to the existence of a neighborhood V of 0 and a compact set K with f''V ⊆ K, under appropriate structural assumptions.

Русский

Для линейного отображения f: M1 → M2 эквивалентно существование окрестности V(0) и компактного K с f''V ⊆ K (при надлежащих условиях).

LaTeX

$$$IsCompactOperator(f) \iff \exists V \in 𝓝(0), \exists K, IsCompact(K) \land f[V] \subseteq K$$$

Lean4

theorem isCompact_closure_image_of_isVonNBounded [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f)
    {S : Set M₁} (hS : IsVonNBounded 𝕜₁ S) : IsCompact (closure <| f '' S) :=
  let ⟨_, hK, hKf⟩ := hf.image_subset_compact_of_isVonNBounded hS
  hK.closure_of_subset hKf

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