instTopologicalSpace

Mathlib.Topology.Order.ScottTopology

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

English

The topology on WithScott α is exactly the Scott topology on α (univ).

Русский

Топология на WithScott α равна скоттовской топологии на α (univ).

LaTeX

$$$\text{TopologicalSpace}(WithScott(\alpha)) = \mathrm{scott}(\alpha,\mathrm{univ}).$$$

Lean4

instance : TopologicalSpace (WithScott α) :=
  scott α univ

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

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

Разделы

Аффилиация

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