Theorems · Theorem · functional analysis

IsModuleTopology.of_continuous_id

∀ {R : Type u_1} [inst : TopologicalSpace R] {A : Type u_2} [inst_1 : Add A] [inst_2 : SMul R A]
  [τA : TopologicalSpace A] [ContinuousAdd A] [ContinuousSMul R A], Continuous id → IsModuleTopology R A

If A is a topological R-module and the identity map from (A with its given topology) to (A with the module topology) is continuous, then the topology on A is the module topology.

Defined in

Mathlib.Topology.Algebra.Module.ModuleTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddSMulTopologicalSpaceContinuousAddContinuousSMul