English
Let M be a monoid acting distributively and continuously on the base field 𝕜, and this action commutes with scalar multiplication on 𝕜. Then M acts continuously on the WeakDual 𝕜 E, i.e., the action map M × WeakDual 𝕜 E → WeakDual 𝕜 E is continuous.
Русский
Пусть моноид M действует дистрибутивно и непрерывно на основание 𝕜, и это действие коммутирует с умножением на 𝕜. Тогда M действует непрерывно на слабом двойственном пространстве WeakDual 𝕜 E: отображение действия M × WeakDual 𝕜 E → WeakDual 𝕜 E непрерывно.
LaTeX
$$$\mu \in C\big(M \times \mathrm{WeakDual}_{\mathbb{k}} E, \mathrm{WeakDual}_{\mathbb{k}} E\big)$$$
Lean4
/-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
multiplication on `𝕜`, then it continuously acts on `WeakDual 𝕜 E`. -/
instance instContinuousSMul (M) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [TopologicalSpace M]
[ContinuousSMul M 𝕜] : ContinuousSMul M (WeakDual 𝕜 E) :=
⟨continuous_induced_rng.2 <|
continuous_fst.smul ((WeakBilin.coeFn_continuous (topDualPairing 𝕜 E)).comp continuous_snd)⟩
