ediam_of_unbounded

Mathlib.Topology.MetricSpace.Bounded

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

English

If s is unbounded, then ediam(s) = ∞.

Русский

Если s неограничено, то ediam(s) = ∞.

LaTeX

$$$\\neg \\operatorname{IsBounded}(s) \\Rightarrow \\operatorname{ediam}(s) = \\infty$$$

Lean4

theorem ediam_of_unbounded (h : ¬IsBounded s) : EMetric.diam s = ∞ :=
  ediam_eq_top_iff_unbounded.2 h

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

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

Разделы

Аффилиация

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