totallyBounded_Ioo

Mathlib.Topology.MetricSpace.Bounded

URI: https://scilib.ai/kg/mathlib#totallyBounded_Ioo

English

The open interval Ioo(a,b) is totally bounded under the same hypotheses as above.

Русский

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

LaTeX

$$TotallyBounded(Ioo(a,b))$$

Lean4

theorem totallyBounded_Ioo (a b : α) : TotallyBounded (Ioo a b) :=
  (totallyBounded_Icc a b).subset Ioo_subset_Icc_self

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

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

Разделы

Аффилиация

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