English
If two submodules have the same topological closure, their closures coincide as sets.
Русский
Если два подмодуля имеют одинаковые топологические замыкания, их множества совпадают.
LaTeX
$$$s.topologicalClosure = t.topologicalClosure \Rightarrow s.set = t.set$$$
Lean4
/-- If `s i` is a family of submodules, each is in its module,
then the closure of their span in the indexed product of the modules
is the product of their closures.
In case of a finite index type, this statement immediately follows from `Submodule.iSup_map_single`.
However, the statement is true for an infinite index type as well.
This version is stated in terms of `Submodule.topologicalClosure`,
thus assumes that `M i`s are topological modules over `R`.
However, the statement is true without assuming continuity of the operations,
see `Submodule.closure_coe_iSup_map_single` above. -/
theorem topologicalClosure_iSup_map_single [∀ i, ContinuousAdd (M i)] [∀ i, ContinuousConstSMul R (M i)]
(s : ∀ i, Submodule R (M i)) :
topologicalClosure (⨆ i, (s i).map (LinearMap.single R M i)) = pi Set.univ fun i ↦ (s i).topologicalClosure :=
SetLike.coe_injective <| closure_coe_iSup_map_single _
