English
Equality between the constructed mkOfIsCompactOperator hf and the original f as linear maps.
Русский
Равенство между сконструированной mkOfIsCompactOperator hf и исходной f как линейных отображений.
LaTeX
$$$(\\mathrm{mkOfIsCompactOperator}(hf) : M_1 \\toₛ[M_1] M_2) = f$$$
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 closed 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'`).
TODO: reformulate this in terms of a type synonym with the right topology. -/
theorem isClosed_image_coe_of_bounded_of_weak_closed {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) :
IsClosed (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' s) :=
isClosed_of_closure_subset fun f hf =>
⟨ofMemClosureImageCoeBounded f hb hf, hc (ofMemClosureImageCoeBounded f hb hf) hf, rfl⟩
