polar — Mathlib

English

The polar of a subset s of E, with respect to 𝕜, is the preimage under the strong dual map of the polar of s in the strong dual.

Русский

Полярная мощь множества s по отношению к 𝕜 определена как предобраз под отображением сильной двойственности множества полярности в StrongDual.

LaTeX

$$$ polar\\, 𝕜\\, s = (toStrongDual)^{-1}(StrongDual.polar\\, 𝕜)(s)$$$

Lean4

/-- The polar set `polar 𝕜 s` of `s : Set E` seen as a subset of the dual of `E` with the
weak-star topology is `WeakDual.polar 𝕜 s`. -/
def polar (s : Set E) : Set (WeakDual 𝕜 E) :=
  toStrongDual ⁻¹' (StrongDual.polar 𝕜) s

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