completeSpace — Mathlib

English

For a family s_i of submodules, the topological closure of the iSup of their maps via single equals the product of their closures.

Русский

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

LaTeX

$$$\operatorname{topologicalClosure}\left(\bigsqcup_i (s_i).map(\text{single})\right) = \pi_i \; \overline{s_i}$$$

Lean4

instance completeSpace {M' : Type*} [AddCommMonoid M'] [Module R M'] [UniformSpace M'] [ContinuousAdd M']
    [ContinuousConstSMul R M'] [CompleteSpace M'] (U : Submodule R M') : CompleteSpace U.topologicalClosure :=
  isClosed_closure.completeSpace_coe

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