isBounded_Ioo

Mathlib.Topology.MetricSpace.Bounded

URI: https://scilib.ai/kg/mathlib#Metric.isBounded_Ioo

English

For any a < b, the open interval Ioo(a,b) is bounded.

Русский

Открытый интервал Ioo(a,b) ограничен.

LaTeX

$$$IsBounded(Ioo(a,b)).$$$

Lean4

theorem isBounded_Ioo (a b : α) : IsBounded (Ioo a b) :=
  (totallyBounded_Ioo a b).isBounded

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

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

Разделы

Аффилиация

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