diam_eq_zero_of_unbounded — Mathlib

English

If s is unbounded, then diam(s) = 0.

Русский

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

LaTeX

$$$\\neg \\operatorname{IsBounded}(s) \\Rightarrow \\operatorname{diam}(s) = 0$$$

Lean4

/-- An unbounded set has zero diameter. If you would prefer to get the value ∞, use `EMetric.diam`.
This lemma makes it possible to avoid side conditions in some situations -/
theorem diam_eq_zero_of_unbounded (h : ¬IsBounded s) : diam s = 0 := by
  rw [diam, ediam_of_unbounded h, ENNReal.toReal_top]

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