polar — Mathlib

English

For a bilinear-type map B: E × F → 𝕜, the polar of a set s ⊆ E is the set of all y ∈ F such that ‖B(x,y)‖ ≤ 1 for every x ∈ s.

Русский

Для билинейной формы B: E × F → 𝕜 поляром множества s ⊆ E является множество всех y ∈ F such that ‖B(x,y)‖ ≤ 1 для каждого x ∈ s.

LaTeX

$$$\mathrm{polar}(s) = \{ y \in F \mid \forall x \in s, \|B(x,y)\| \le 1 \}$$$

Lean4

/-- The (absolute) polar of `s : Set E` is given by the set of all `y : F` such that `‖B x y‖ ≤ 1`
for all `x ∈ s`. -/
def polar (s : Set E) : Set F :=
  {y : F | ∀ x ∈ s, ‖B x y‖ ≤ 1}

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