topologicalClosure — Mathlib

English

The closure of a submodule S in a topological R-module M is again a submodule of M.

Русский

Замыкание подмодуля S в топологическом R-модуле M снова является подмодулем M.

LaTeX

$$$\text{topologicalClosure}(S) \\text{is a submodule of } M$$$

Lean4

/-- The (topological-space) closure of a submodule of a topological `R`-module `M` is itself
a submodule. -/
def topologicalClosure (s : Submodule R M) : Submodule R M :=
  { s.toAddSubmonoid.topologicalClosure with smul_mem' := s.mapsTo_smul_closure }

Похожие утверждения