isClosed_topologicalClosure

Mathlib.Topology.Algebra.Ring.Basic

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

English

The topological closure of a subring is always a closed set in the ambient space.

Русский

Топологическое замыкание подкольца всегда является закрытым подмножеством в окружающем пространстве.

LaTeX

$$IsClosed (S_{topologicalClosure})$$

Lean4

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

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

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

Разделы

Аффилиация

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