English
If A is a locally convex R-module and B is another R-module, and e: A ≃L[R] B is an R-linear homeomorphism, then B carries the module topology.
Русский
Если A и B — R-модули, между ними есть R-линиейный гомоморфизм-изоморфизм e, то если A имеет модульную топологию, то ее имеет и B.
LaTeX
$$$\text{IsModuleTopology } R B \;\text{given } e: A \simeq_{L[R]} B \text{ and } \text{IsModuleTopology } R A$$$
Lean4
/-- The module topology, for a module `A` over a topological ring `R`. It's the finest topology
making addition and the `R`-action continuous, or equivalently the finest topology making `A`
into a topological `R`-module. More precisely it's the Inf of the set of
topologies with these properties; theorems `continuousSMul` and `continuousAdd` show
that the module topology also has these properties. -/
abbrev moduleTopology : TopologicalSpace A :=
sInf {t | @ContinuousSMul R A _ _ t ∧ @ContinuousAdd A t _}
