Theorems · Theorem · functional analysis

NormedSpace.isCompact_closure_of_isBounded

∀ (𝕜 : Type u_3) [inst : RCLike 𝕜] (X : Type u_4) [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace 𝕜 X]
  (S : Set (WeakSpace 𝕜 X)),
  Bornology.IsBounded (⇑(toWeakSpace 𝕜 X) ⁻¹' S) →
    closure (⇑(NormedSpace.inclusionInDoubleDualWeak 𝕜 X) '' S) ⊆
        Set.range ⇑(NormedSpace.inclusionInDoubleDualWeak 𝕜 X) →
      IsCompact (closure S)

If S is bounded set in WeakSpace X and the weak-star closure of its image under the embedding into the weak-star double dual lies in the range of that embedding, then closure S is compact in the weak topology. This combines Banach–Alaoglu (compactness of bounded weak-star–closed sets) with the topological embedding inclusionInDoubleDualWeak_isEmbedding to transfer compactness back to the weak topology on X.

Defined in

Mathlib.Analysis.Normed.Module.DoubleDual

Cited by

0 results in Mathlib

Foundations

Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupNormedSpace