dirSupClosed_of_isClosed

Mathlib.Topology.Order.ScottTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsScott.dirSupClosed_of_isClosed

English

If s is an upper set in IsScott α univ, then s is closed.

Русский

Если s является верхним множеством в IsScott α univ, то оно замкнуто.

LaTeX

$$$IsUpperSet(s) \\Rightarrow IsClosed(s)$$$

Lean4

theorem dirSupClosed_of_isClosed [IsScott α univ] : IsClosed s → DirSupClosed s := fun h ↦
  (isClosed_iff_isLowerSet_and_dirSupClosed.mp h).right

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

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

Разделы

Аффилиация

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