isClosed_image_coe_of_bounded_of_closed

English

Let s be a subset of WeakDual 𝕜 E. If s is closed and bounded in the weak topology and its preimage under the weak-strong dual map is bounded, then s is compact.

Русский

Пусть s ⊆ WeakDual 𝕜 E. Если s замкнуто и ограничено в слабой топологии, а его предобраз под слабой-двойственной картиной ограничено, то s компактно.

LaTeX

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

Lean4

/-- While the coercion `↑ : WeakDual 𝕜 E → (E → 𝕜)` is not a closed map, it sends *bounded*
closed sets to closed sets. -/
theorem isClosed_image_coe_of_bounded_of_closed {s : Set (WeakDual 𝕜 E)} (hb : IsBounded (StrongDual.toWeakDual ⁻¹' s))
    (hc : IsClosed s) : IsClosed (((↑) : WeakDual 𝕜 E → E → 𝕜) '' s) :=
  ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed hb (isClosed_induced_iff'.1 hc)

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