English
The weak space on E is the coarsest topology making every continuous linear functional φ(x)=v x continuous; equivalently it is the initial topology induced by the dual pairing.
Русский
Слабая пространство на V является самой грубой топологией, которая делает непрерывными все линейные функционалы φ(x)=v(x); эквивалентно это начальная топология, индуцированная двойственной парой.
LaTeX
$$$\\tau_{\\mathrm{weak}}(E) = \\operatorname{init}_{\\varphi \\in E'} (\\tau_{\\varphi})$$$
Lean4
/-- The weak topology is the topology coarsest topology on `E` such that all functionals
`fun x => v x` are continuous. -/
def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E]
[Module 𝕜 E] [TopologicalSpace E] :=
WeakBilin (topDualPairing 𝕜 E).flip
deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
