mem_polar_iff — Mathlib

English

Let x' be in the strong dual of E and s ⊆ E. Then x' lies in polar 𝕜 s if and only if for every z ∈ s we have ‖x'(z)‖ ≤ 1.

Русский

Пусть x' ∈ сильного двойственного пространства E и s ⊆ E. Тогда x' принадлежит полю 𝕜 s тогда и только тогда, когда для каждого z ∈ s выполняется ‖x'(z)‖ ≤ 1.

LaTeX

$$$x' \in \operatorname{polar}_{\mathbb{K}}(s) \iff \forall z \in s, \|x'(z)\| \le 1$$$

Lean4

theorem mem_polar_iff {x' : StrongDual 𝕜 E} (s : Set E) : x' ∈ polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1 :=
  Iff.rfl

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