totallyBounded_Ioc

Mathlib.Topology.MetricSpace.Bounded

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

English

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

Русский

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

LaTeX

$$TotallyBounded(Ioc(a,b))$$

Lean4

theorem totallyBounded_Ioc (a b : α) : TotallyBounded (Ioc a b) :=
  (totallyBounded_Icc a b).subset Ioc_subset_Icc_self

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

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

Разделы

Аффилиация

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