English
Every R-linear map between two topological R-modules, where the source has the module topology, is continuous.
Русский
Каждое R-линейное отображение между двумя топологическими R-модулями, если источнику присвоена модульная топология, является непрерывным.
LaTeX
$$$\text{continuous_of_distribMulActionHom}(\varphi) : Continuous(\varphi)$$$
Lean4
/-- Every `R`-linear map between two topological `R`-modules, where the source has the module
topology, is continuous. -/
@[fun_prop, continuity]
theorem continuous_of_distribMulActionHom (φ : A →+[R] B) : Continuous φ := by
-- the proof: We know that `+ : B × B → B` and `• : R × B → B` are continuous for the module
-- topology on `B`, and two earlier theorems (`continuousSMul_induced` and
-- `continuousAdd_induced`) say that hence `+` and `•` on `A` are continuous if `A`
-- is given the topology induced from `φ`. Hence the module topology is finer than
-- the induced topology, and so the function is continuous.
rw [eq_moduleTopology R A, continuous_iff_le_induced]
exact sInf_le <| ⟨continuousSMul_induced (φ.toMulActionHom), continuousAdd_induced φ.toAddMonoidHom⟩
