instT5Space

Mathlib.Topology.Order.Real

URI: https://scilib.ai/kg/mathlib#EReal.instT5Space

English

The extended real line EReal is equipped with the order topology coming from its natural order.

Русский

Удлинённая действительная линейка EReal снабжена порядковой топологией, соответствующей её естественному порядку.

LaTeX

$$$\\text{TopologicalSpace}(EReal) = \\text{Preorder.topology}(EReal).$$$

Lean4

instance : T5Space EReal :=
  inferInstance

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

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

Разделы

Аффилиация

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