English
Banach–Alaoglu: for any x' ∈ StrongDual 𝕜 E and r ∈ ℝ, the preimage under the canonical map of the closed ball of radius r around x' is compact in WeakDual 𝕜 E.
Русский
Теорема Банаха–Алаоглу: для любого x' ∈ StrongDual 𝕜 E и радиуса r ∈ ℝ, множество \\( (toStrongDual)^{-1}( \\overline{B}(x', r) ) \\) замкнуто по слабой звёздочной топологии в WeakDual 𝕜 E и компактно.
LaTeX
$$$IsCompact\\left( (toStrongDual)^{-1}\\left( closedBall x' r \\right) \\right)$$$
Lean4
/-- The **Banach-Alaoglu theorem**: closed balls of the dual of a normed space `E` are compact in
the weak-star topology. -/
theorem isCompact_closedBall [ProperSpace 𝕜] (x' : StrongDual 𝕜 E) (r : ℝ) :
IsCompact (toStrongDual ⁻¹' closedBall x' r) :=
isCompact_of_bounded_of_closed isBounded_closedBall (isClosed_closedBall x' r)
