isCompact_of_bounded_of_closed — Mathlib

English

Under a stronger assumption (ProperSpace 𝕜), the same compactness conclusion holds for s ⊆ WeakDual 𝕜 E.

Русский

При более сильном предположении (ProperSpace 𝕜) те же выводы компактности справедливы для s ⊆ WeakDual 𝕜 E.

LaTeX

$$$\\text{IsCompact}(s) \\text{ under } \\text{ProperSpace } 𝕜 \\land (IsBounded(StrongDual.toWeakDual^{-1}'(s)) \\land IsClosed(s))$$$

Lean4

theorem isCompact_of_bounded_of_closed [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)}
    (hb : IsBounded (StrongDual.toWeakDual ⁻¹' s)) (hc : IsClosed s) : IsCompact s :=
  DFunLike.coe_injective.isEmbedding_induced.isCompact_iff.mpr <|
    ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image hb <|
      isClosed_image_coe_of_bounded_of_closed hb hc

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