isCompact_polar — Mathlib

English

Banach–Alaoglu theorem: the polar set of a neighborhood s of the origin in a normed space E is a compact subset of WeakDual 𝕜 E.

Русский

Теорема Банаха–Алаоглу: полярное множество polar 𝕜 s окрестности нуля в нормированном пространстве E компактно внутри WeakDual 𝕜 E.

LaTeX

$$$IsCompact\\left( polar 𝕜 s \\right)$$$

Lean4

/-- The **Banach-Alaoglu theorem**: the polar set of a neighborhood `s` of the origin in a
normed space `E` is a compact subset of `WeakDual 𝕜 E`. -/
theorem isCompact_polar [ProperSpace 𝕜] {s : Set E} (s_nhds : s ∈ 𝓝 (0 : E)) : IsCompact (polar 𝕜 s) :=
  isCompact_of_bounded_of_closed (isBounded_polar_of_mem_nhds_zero 𝕜 s_nhds) (isClosed_polar _ _)

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