instTopologicalSpace

Mathlib.SetTheory.Ordinal.Topology

URI: https://scilib.ai/kg/mathlib#Ordinal.instTopologicalSpace

English

A TopologicalSpace structure is defined on ordinals via the preorder topology.

Русский

Топологическая структура на ординалах задается через топологию по частному порядку.

LaTeX

$$TopologicalSpace Ordinal := Preorder.topology Ordinal$$

Lean4

instance : TopologicalSpace Ordinal.{u} :=
  Preorder.topology Ordinal.{u}

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

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

Разделы

Аффилиация

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