English
The Strong Dual of a topological module M over a ring R is the space of continuous linear maps M → R, i.e., the space of continuous linear functionals, denoted M →L[R] R.
Русский
Сильный двойственный модуль — это пространство непрерывно линейных функционалов, то есть отображений M → R, с пометкой S := M →L[R] R.
LaTeX
$$$\\text{StrongDual}(R,M) := M \\to_L[R] R$$$
Lean4
/-- 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`. -/
abbrev StrongDual (R : Type*) [Semiring R] [TopologicalSpace R] (M : Type*) [TopologicalSpace M] [AddCommMonoid M]
[Module R M] : Type _ :=
M →L[R] R
