isClosed_polar — Mathlib

English

The polar of any set in a normed space is a closed set in the dual space.

Русский

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

LaTeX

$$$\\operatorname{IsClosed}(\\operatorname{StrongDual.polar} 𝕜 s)$$$

Lean4

theorem isClosed_polar (s : Set E) : IsClosed (StrongDual.polar 𝕜 s) :=
  by
  dsimp only [StrongDual.polar]
  simp only [LinearMap.polar_eq_iInter, LinearMap.flip_apply]
  refine isClosed_biInter fun z _ => ?_
  exact isClosed_Iic.preimage (ContinuousLinearMap.apply 𝕜 𝕜 z).continuous.norm

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