polar_isClosed — Mathlib

English

For every s, the polar set B.polar(s) is closed in the ambient topology on F.

Русский

Для каждого множества s полярное множество B.polar(s) замкнуто в данной топологии на F.

LaTeX

$$IsClosed(B.polar(s))$$

Lean4

theorem polar_isClosed (s : Set E) : IsClosed (X := WeakBilin B.flip) (B.polar s) :=
  by
  rw [polar_eq_biInter_preimage]
  exact isClosed_biInter fun _ _ ↦ Metric.isClosed_closedBall.preimage (WeakBilin.eval_continuous B.flip _)

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