instTopologicalSpace

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithUpperSet.instTopologicalSpace

English

The topology on WithUpperSet α is defined by upper sets as open sets.

Русский

Топология на WithUpperSet(α) задаётся так, что открытыми являются верхние множества.

LaTeX

$$$\text{TopSpace}(\mathrm{WithUpperSet}(\alpha))\;\text{is defined by }\mathrm{IsOpen}(U) \iff U \text{ is an upper set in } \alpha$$$

Lean4

instance : TopologicalSpace (WithUpperSet α) :=
  upperSet α

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

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

Разделы

Аффилиация

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