isClosed_topologicalClosure

Mathlib.Topology.Algebra.Module.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.isClosed_topologicalClosure

English

If S ⊆ T and T is closed, then the topological closure of S is contained in T.

Русский

Если S ⊆ T и T замкнуто, то топологическое замыкание S содержится в T.

LaTeX

$$$S \le T \quad \&\quad IsClosed(T) \Rightarrow S.topologicalClosure \le T$$$

Lean4

theorem isClosed_topologicalClosure (s : Submodule R M) : IsClosed (s.topologicalClosure : Set M) :=
  isClosed_closure

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru