polar_def — Mathlib

English

The polar of s is the set of functionals that send every x ∈ s to a value with magnitude at most 1.

Русский

Поляр множества s состоит из функционалов, которые отображают каждый x ∈ s в значения с модулем не более 1.

LaTeX

$$$polar\\, 𝕜\\, s = \\{ f: WeakDual 𝕜 E \\mid \\forall x \\in s, \\|f(x)\\| \\le 1\\}$$$

Lean4

theorem polar_def (s : Set E) : polar 𝕜 s = {f : WeakDual 𝕜 E | ∀ x ∈ s, ‖f x‖ ≤ 1} :=
  rfl

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