polar_univ — Mathlib

English

The polar of the entire space is the zero functional: polar 𝕜 univ = {0}.

Русский

Поляр всей области есть нулевой функционал: polar 𝕜 univ = {0}.

LaTeX

$$$\operatorname{polar}_{\mathbb{K}}(\mathrm{univ}) = \{0\}$$$

Lean4

@[simp]
theorem polar_univ : polar 𝕜 (univ : Set E) = {(0 : StrongDual 𝕜 E)} :=
  (topDualPairing 𝕜 E).flip.polar_univ (LinearMap.flip_separatingRight.mpr (dualPairing_separatingLeft 𝕜 E))

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