Theorems · Theorem · functional analysis

IsModuleTopology.continuous_of_distribMulActionHom

∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Semiring R] {A : Type u_3} [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_4} [inst_4 : AddCommMonoid B]
  [inst_5 : Module R B] [aB : TopologicalSpace B] [ContinuousAdd B] [ContinuousSMul R B] (φ : A →+[R] B), Continuous ⇑φ

Every R-linear map between two topological R-modules, where the source has the module topology, is continuous.

Defined in

Mathlib.Topology.Algebra.Module.ModuleTopology

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceSemiringAddCommMonoidModuleTopologicalSpaceIsModuleTopologyAddCommMonoidModuleTopologicalSpaceContinuousAddContinuousSMul