Theorems · Theorem · functional analysis

Submodule.closure_coe_iSup_map_single

∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : (i : ι) → TopologicalSpace (M i)] [inst_4 : DecidableEq ι]
  (s : (i : ι) → Submodule R (M i)),
  closure ↑(⨆ i, Submodule.map (LinearMap.single R M i) (s i)) = Set.univ.pi fun i => closure ↑(s i)

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.

Defined in

Mathlib.Topology.Algebra.Module.Basic

Cited by

1 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleTopologicalSpaceDecidableEq