totallyBounded_Ico

Mathlib.Topology.MetricSpace.Bounded

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

English

The half-open interval Ico(a,b) is totally bounded in a uniform space with a preorder and CompactIccSpace.

Русский

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

LaTeX

$$TotallyBounded(Ico(a,b))$$

Lean4

theorem totallyBounded_Ico (a b : α) : TotallyBounded (Ico a b) :=
  (totallyBounded_Icc a b).subset Ico_subset_Icc_self

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

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

Разделы

Аффилиация

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