polarSubmodule — Mathlib

English

The polar of a set closed under scalar multiplication can be identified with an infimum-based submodule in F.

Русский

Поляр множества, замкнутого относительно масштабирования, может быть идентифицирована с подмодулем в F через инфимуум.

LaTeX

$$polarSubmodule(B)(s) = ⨅ x∈s ker(Bx) ∥ Bpolar ∼$$

Lean4

/-- The polar of a set closed under scalar multiplication as a submodule -/
def polarSubmodule {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : Submodule 𝕜 F :=
  .copy (⨅ x ∈ m, LinearMap.ker (B x)) (B.polar m) <| by ext; simp [polar_subMulAction]

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