English
WeakDual 𝕜 E is the weak star topology on E induced by the topDualPairing 𝕜 E; it is a canonical construction setting E into a dual-like object with weak topology.
Русский
WeakDual 𝕜 E — это слабая звёздочная топология на E, индуцированная парой сопряжений topDualPairing 𝕜 E; это каноническая конструкция, помещающая E в объект, подобный двойственному пространству с слабой топологией.
LaTeX
$$def WeakDual (𝕜 E) := WeakBilin (topDualPairing 𝕜 E)$$
Lean4
/-- The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
functionals `fun v => v x` are continuous. -/
def WeakDual (𝕜 E : Type*) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜]
[AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
WeakBilin (topDualPairing 𝕜 E)
deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited, FunLike, ContinuousLinearMapClass
