isClosed_of_isUpperSet

Mathlib.Topology.Order.ScottTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsScottHausdorff.isClosed_of_isUpperSet

English

In a Scott space IsScott α univ, an upper set is closed.

Русский

В пространстве Скотта верхнее множество закрыто.

LaTeX

$$$\\text{IsUpperSet}(s) \\Rightarrow \\text{IsClosed}(s)$$$

Lean4

theorem isClosed_of_isUpperSet (h : IsUpperSet s) : IsClosed s :=
  isOpen_compl_iff.1 <| isOpen_of_isLowerSet h.compl

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

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

Разделы

Аффилиация

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