ediam_eq_top_iff_unbounded

Mathlib.Topology.MetricSpace.Bounded

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

English

ediam s = ∞ iff not IsBounded s.

Русский

ediam s = ∞ если и только если не является ограниченным.

LaTeX

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

Lean4

theorem ediam_eq_top_iff_unbounded : EMetric.diam s = ⊤ ↔ ¬IsBounded s :=
  isBounded_iff_ediam_ne_top.not_left.symm

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

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

Разделы

Аффилиация

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