polar_mem_iff — Mathlib

English

For any s ⊆ E and y ∈ F, y lies in the polar of s if and only if for all x ∈ s, ‖B x y‖ ≤ 1.

Русский

Пусть s ⊆ E, y ∈ F. Тогда y принадлежит полярe s тогда и только тогда, когда для всех x ∈ s выполнено ‖B x y‖ ≤ 1.

LaTeX

$$$y \in B.polar(s) \iff \forall x \in s, \|B(x,y)\| \le 1$$$

Lean4

theorem polar_mem_iff (s : Set E) (y : F) : y ∈ B.polar s ↔ ∀ x ∈ s, ‖B x y‖ ≤ 1 :=
  Iff.rfl

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