isClosed_topologicalClosure

Mathlib.Topology.Algebra.Field

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

English

For any subfield s of α, the underlying set of its topological closure is a closed subset of α.

Русский

Для любого подполе s ⊆ α множество подзамыкания s.topologicalClosure замкнуто в α.

LaTeX

$$IsClosed\left(s.topologicalClosure : Set \alpha\right)$$

Lean4

theorem isClosed_topologicalClosure (s : Subfield α) : IsClosed (s.topologicalClosure : Set α) :=
  isClosed_closure

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

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

Разделы

Аффилиация

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