instOrderTopology

Mathlib.Topology.Instances.Rat

URI: https://scilib.ai/kg/mathlib#Rat.instOrderTopology

English

ℚ is equipped with the order topology.

Русский

ℚ обладает порядковой топологией.

LaTeX

$$$\\operatorname{OrderTopology}(\\mathbb{Q})$$$

Lean4

instance : OrderTopology ℚ :=
  induced_orderTopology _ Rat.cast_lt exists_rat_btwn

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

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

Разделы

Аффилиация

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