English
If there is a continuous scalar action defining negation on M, then negation is continuous on M by that action.
Русский
Если существует непрерывное действие скаляров, задающее отрицание на M, то отрицание непрерывно в M через это действие.
LaTeX
$$$\\text{ContinuousNeg}(M)$ with the given ContinuousConstSMul$$
Lean4
theorem of_nhds_zero [IsTopologicalRing R] [IsTopologicalAddGroup M]
(hmul : Tendsto (fun p : R × M => p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0))
(hmulleft : ∀ m : M, Tendsto (fun a : R => a • m) (𝓝 0) (𝓝 0))
(hmulright : ∀ a : R, Tendsto (fun m : M => a • m) (𝓝 0) (𝓝 0)) : ContinuousSMul R M where
continuous_smul := by
rw [← nhds_prod_eq] at hmul
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_ <;> simpa [ContinuousAt]
