Theorems · Definition · functional analysis

StrongDual

(R : Type u_1) →
  [inst : Semiring R] →
    [TopologicalSpace R] →
      (M : Type u_2) → [TopologicalSpace M] → [inst_3 : AddCommMonoid M] → [Module R M] → Type (max u_1 u_2)

The strong dual of a topological vector space M over a ring R. This is the space of continuous linear functionals and is equipped with the topology of uniform convergence on bounded subsets. StrongDual R M is an abbreviation for M →L[R] R.

Defined in

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Cited by

459 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 144 definitions · uses no axioms

Assumes

SemiringTopologicalSpaceTopologicalSpaceAddCommMonoidModule