ediam_univ_of_noncompact

Mathlib.Topology.MetricSpace.Bounded

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

← MathLib Explorer

English

If α is a proper and noncompact space, then ediam(univ) = ∞.

Русский

Если пространство α корректно и не компактно, то ediam(univ) = ∞.

LaTeX

$$$\\operatorname{ediam}(\\operatorname{univ}) = \\infty$$$

Lean4

@[simp]
theorem ediam_univ_of_noncompact [ProperSpace α] [NoncompactSpace α] : EMetric.diam (univ : Set α) = ∞ :=
  ediam_univ_eq_top_iff_noncompact.mpr ‹_›

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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