diam_univ_of_noncompact

Mathlib.Topology.MetricSpace.Bounded

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

English

If α is proper and noncompact, then diam(univ) = 0.

Русский

Если пространство корректно и не компактно, то диаметр универсума равен 0.

LaTeX

$$$\\operatorname{diam}(\\operatorname{univ}) = 0$$$

Lean4

@[simp]
theorem diam_univ_of_noncompact [ProperSpace α] [NoncompactSpace α] : diam (univ : Set α) = 0 := by simp [diam]

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

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

Разделы

Аффилиация

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