isCompact_image_coe_of_bounded_of_weak_closed

English

If hb is bounded and hc holds for the weak-closed image, then the image is compact.

Русский

При ограниченности hb и условии hc для слабого замкнутого образа образ является компактным.

LaTeX

$$$\\mathrm{IsCompact}(((\\uparrow) : (E' \\toSL[\\sigma_{12}] F) \\to E' \\to F) '' s)$$$

Lean4

/-- If a set `s` of semilinear functions is bounded and is closed in the weak-* topology, then its
image under coercion to functions `E → F` is a compact set. We don't have a name for `E →SL[σ] F`
with weak-* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`).
-/
theorem isCompact_image_coe_of_bounded_of_weak_closed [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : IsBounded s)
    (hc : ∀ f : E' →SL[σ₁₂] F, (⇑f : E' → F) ∈ closure (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s) → f ∈ s) :
    IsCompact (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s) :=
  isCompact_image_coe_of_bounded_of_closed_image hb <| isClosed_image_coe_of_bounded_of_weak_closed hb hc

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