polarSubmodule_eq_polar — Mathlib

English

For a SubMulAction m, the polarSubmodule 𝕜 m coincides with the polar 𝕜 m; i.e., functionals vanishing on m form the same set as those with norm ≤ 1 on m.

Русский

Для SubMulAction m полярSubmodule 𝕜 m совпадает с поляром 𝕜 m; то есть функционалы, обращающиеся в ноль на m, образуют тот же набор, что и функционалы, удовлетворяющие норме ≤ 1 на m.

LaTeX

$$$\operatorname{polarSubmodule}_{\mathbb{K}}(m) = \operatorname{polar}_{\mathbb{K}}(m) \,$$$

Lean4

theorem polarSubmodule_eq_polar (m : SubMulAction 𝕜 E) : (polarSubmodule 𝕜 m : Set (StrongDual 𝕜 E)) = polar 𝕜 m :=
  rfl

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