totallyBounded_singleton

Mathlib.Topology.UniformSpace.Cauchy

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

English

A singleton is totally bounded.

Русский

Один элемент множества — полностью ограничен.

LaTeX

$$$$\\{a\\} \\text{ is totally bounded}. $$$$

Lean4

@[simp]
theorem totallyBounded_singleton (a : α) : TotallyBounded { a } :=
  (finite_singleton a).totallyBounded

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

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

Разделы

Аффилиация

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