polar_closure — Mathlib

English

Polar of the closure equals polar of the set.

Русский

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

LaTeX

$$$\\operatorname{polar}(𝕜, \\overline{s}) = \\operatorname{polar}(𝕜, s)$$$

Lean4

@[simp]
theorem polar_closure (s : Set E) : StrongDual.polar 𝕜 (closure s) = StrongDual.polar 𝕜 s :=
  ((topDualPairing 𝕜 E).flip.polar_antitone subset_closure).antisymm <|
    (topDualPairing 𝕜 E).flip.polar_gc.l_le <|
      closure_minimal ((topDualPairing 𝕜 E).flip.polar_gc.le_u_l s) <| by
        simpa [LinearMap.flip_flip] using (isClosed_polar _ _).preimage (inclusionInDoubleDual 𝕜 E).continuous

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