English
The topology on M given by a ModuleFilterBasis BR on a module M is the topology obtained from BR's AddGroupFilterBasis, i.e., the zero-neighborhoods are BR.topology's neighborhoods translated to M.
Русский
Топология на M, заданная ModuleFilterBasis BR, получается из AddGroupFilterBasis BR; нулевая окрестность задаётся через топологию BR и переносится на M.
LaTeX
$$$\text{ModuleFilterBasis.topology }(R,M,B) : \text{TopologicalSpace } M$.$$
Lean4
/-- The topology associated to a module filter basis on a module over a topological ring.
It has the given basis as a basis of neighborhoods of zero. This version gets the ring
topology by unification instead of type class inference. -/
def topology' {R M : Type*} [CommRing R] {_ : TopologicalSpace R} [AddCommGroup M] [Module R M]
(B : ModuleFilterBasis R M) : TopologicalSpace M :=
B.toAddGroupFilterBasis.topology
