submodule_topologicalClosure_eq — Mathlib

English

For a family s_i of submodules in a product, the topological closure of the iSup of their maps via single preserves product-of-closures: it equals the product of closures.

Русский

Для семейства подмодулей s_i в произведении верно: замыкание iSup отображений через единичный линейный отображатель равно произведению их замыканий.

LaTeX

$$$\text{topologicalClosure}\left(\big\lceil i \mapsto (s_i).map(\text{single})\big\rceil\right) = \pi_i \; \overline{s_i}$$$

Lean4

/-- The topological closure of a closed submodule `s` is equal to `s`. -/
theorem submodule_topologicalClosure_eq {s : Submodule R M} (hs : IsClosed (s : Set M)) : s.topologicalClosure = s :=
  SetLike.ext' hs.closure_eq

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