English
Let E be a normed space over a nontrivially normed field 𝕜, and let s be a neighborhood of the origin in E. Then the image of polar 𝕜 s under the canonical map from WeakDual 𝕜 E to E → 𝕜 is a closed subset of the space of linear functionals on E.
Русский
Пусть E — нормированное пространство над ненулевой нормированной полем 𝕜, и пусть s — окрестность нуля в E. Тогда образ полярного множества polar 𝕜 s под каноническим отображением WeakDual 𝕜 E в E → 𝕜 образует замкнутое подмножество множества линейных функционалов на E.
LaTeX
$$$IsClosed\\left( \\{ f : E \\to \\mathbb{K} \\mid \\exists \\phi \\in polar 𝕜(s), f = \\phi \\} \\right)$$$
Lean4
/-- The image under `↑ : WeakDual 𝕜 E → (E → 𝕜)` of a polar `WeakDual.polar 𝕜 s` of a
neighborhood `s` of the origin is a closed set. -/
theorem isClosed_image_polar_of_mem_nhds {s : Set E} (s_nhds : s ∈ 𝓝 (0 : E)) :
IsClosed (((↑) : WeakDual 𝕜 E → E → 𝕜) '' polar 𝕜 s) :=
isClosed_image_coe_of_bounded_of_closed (isBounded_polar_of_mem_nhds_zero 𝕜 s_nhds) (isClosed_polar _ _)
