isOpen

Mathlib.Topology.Order.Basic

URI: https://scilib.ai/kg/mathlib#IsUpperSet.isOpen

English

In an OrderTopology α with WellFoundedLT α, every open nonempty set contains a nonempty open interval Ioo(a,b).

Русский

В OrderTopology α с WellFoundedLT α каждое непустое открытое множество содержит ненулевой открытый интервал Ioo(a,b).

LaTeX

$$$\\exists a,b\\ (a

Lean4

theorem isOpen [OrderTopology α] [WellFoundedGT α] {s : Set α} (h : IsUpperSet s) : IsOpen s :=
  h.toDual.isOpen

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

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

Разделы

Аффилиация

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