isClosed_polar — Mathlib

English

The polar of any subset s is a closed set in the weak-star topology.

Русский

Поляр любого множества является замкнутым множеством в слабой топологии.

LaTeX

$$$IsClosed(Polar\\, 𝕜\\, s)$$$

Lean4

/-- The polar `polar 𝕜 s` of a set `s : E` is a closed subset when the weak star topology
is used. -/
theorem isClosed_polar (s : Set E) : IsClosed (polar 𝕜 s) :=
  by
  simp only [polar_def, setOf_forall]
  exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm

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