closure_subset_topologicalClosure_span

English

For any set S, the closure of S is contained in the topological closure of the span of S.

Русский

Для множества S замыкание S содержится в топологическом замыкании Оболочки над S.

LaTeX

$$$\overline{S} \subseteq (\operatorname{span}_R S)^{topologicalClosure}$$$

Lean4

theorem closure_subset_topologicalClosure_span (s : Set M) : closure s ⊆ (span R s).topologicalClosure :=
  by
  rw [Submodule.topologicalClosure_coe]
  exact closure_mono subset_span

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