instIsOrderBornology

Mathlib.Topology.Bornology.Real

URI: https://scilib.ai/kg/mathlib#Real.instIsOrderBornology

English

The real line ℝ is an order-bornology.

Русский

Реальная прямая ℝ является порядковой борнолгией.

LaTeX

$$$IsOrderBornology \\mathbb{R}$$$

Lean4

instance instIsOrderBornology : IsOrderBornology ℝ :=
  .of_isCompactIcc 0 (by simp [closedBall_eq_Icc]) (by simp [closedBall_eq_Icc])

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

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

Разделы

Аффилиация

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