Theorems · Definition · functional analysis

StrongDual.polar

(R : Type u_4) →
  [inst : NormedCommRing R] →
    {M : Type u_5} →
      [inst_1 : AddCommMonoid M] → [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → Set M → Set (StrongDual R M)

Given a subset s in a monoid M (over a commutative ring R), the polar polar R s is the subset of StrongDual R M consisting of those functionals which evaluate to something of norm at most one at all points z ∈ s.

Defined in

Mathlib.Analysis.LocallyConvex.Polar

Cited by

19 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedCommRingAddCommMonoidTopologicalSpaceModule