instTopologicalSpace

Mathlib.Topology.Order.UpperLowerSetTopology

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

English

WithLowerSet α carries the lower-set topology.

Русский

WithLowerSet α оснащён топологией нижних множеств.

LaTeX

$$$ \operatorname{TopologicalSpace}(\mathrm{WithLowerSet}\alpha) = \mathrm{lowerSet}\alpha.$$$

Lean4

instance : TopologicalSpace (WithLowerSet α) :=
  lowerSet α

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

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

Разделы

Аффилиация

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