polarSubmodule_eq_setOf — Mathlib

English

The polarSubmodule 𝕜 m is equal to the set of all y ∈ StrongDual 𝕜 E such that ∀ x ∈ E, if x ∈ m then y(x) = 0.

Русский

polarSubmodule 𝕜 m равен множеству всех y ∈ StrongDual 𝕜 E таких, что для всех x ∈ E, если x ∈ m, то y(x) = 0.

LaTeX

$$$\operatorname{polarSubmodule}_{\mathbb{K}}(m) = \{ y \in \mathrm{StrongDual}_{\mathbb{K}}(E) \mid \forall x \in E,\ x \in m \Rightarrow y(x)=0 \}$$$

Lean4

theorem polarSubmodule_eq_setOf {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) :
    polarSubmodule 𝕜 m = {y : StrongDual 𝕜 E | ∀ x ∈ m, y x = 0} :=
  (topDualPairing 𝕜 E).flip.polar_subMulAction _

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