isClosed_image_polar_of_mem_nhds — Mathlib

English

Let s be a neighborhood of the origin in E. The image of polar 𝕜 s under the canonical map from StrongDual 𝕜 E to E → 𝕜 is closed in the space of linear functionals on E.

Русский

Пусть s — окрестность нуля в E. Тогда образ полярной polar 𝕜 s под каноническим отображением StrongDual 𝕜 E в E → 𝕜 замкнут в пространстве линейных функционалов на E.

LaTeX

$$$IsClosed\\left( \\{ f : E \\to \\mathbb{K} \\mid \\exists \\phi \\in polar 𝕜 s, f = \\phi \\} \\right)$$$

Lean4

/-- The image under `↑ : StrongDual 𝕜 E → (E → 𝕜)` of a polar `polar 𝕜 s` of a
neighborhood `s` of the origin is a closed set. -/
theorem _root_.NormedSpace.Dual.isClosed_image_polar_of_mem_nhds {s : Set E} (s_nhds : s ∈ 𝓝 (0 : E)) :
    IsClosed (((↑) : StrongDual 𝕜 E → E → 𝕜) '' StrongDual.polar 𝕜 s) :=
  WeakDual.isClosed_image_polar_of_mem_nhds 𝕜 s_nhds

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