isOpen_of_isLowerSet

Mathlib.Topology.Order.ScottTopology

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

← MathLib Explorer

English

In a Scott space IsScott α univ, every lower set is open.

Русский

В пространстве Скотта IsScott α univ каждый нижний множество открыто.

LaTeX

$$$\\text{IsLowerSet}(s) \\Rightarrow \\text{IsOpen}(s)$$$

Lean4

theorem isOpen_of_isLowerSet (h : IsLowerSet s) : IsOpen s :=
  (isOpen_iff (D := univ)).2 fun _d _ ⟨b, hb⟩ _ _ hda ha ↦ ⟨b, hb, fun _ hc ↦ h (mem_upperBounds.1 hda.1 _ hc.2) ha⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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