toContinuousAdd — Mathlib

English

If A is a locally convex R-module, then the action R × A → A is continuous with respect to the module topology.

Русский

Если A — локально выпуклый R-модуль, то действие R × A → A непрерывно в модульной топологии.

LaTeX

$$$\text{ContinuousSMul } R A\ (\text{moduleTopology } R A)$$$

Lean4

theorem toContinuousAdd [TopologicalSpace A] [IsModuleTopology R A] : ContinuousAdd A :=
  eq_moduleTopology R A ▸ ModuleTopology.continuousAdd R A

Похожие утверждения