diam — Mathlib

English

The diameter of a set is defined as the real-valued realization of its metric diameter.

Русский

Диаметр множества определяется как вещевая реализация метрического диаметра.

LaTeX

$$$\\operatorname{diam}(s) = \\operatorname{ENNReal.toReal}(\\operatorname{EMetric.diam}(s)).$$$

Lean4

/-- The diameter of a set in a metric space. To get controllable behavior even when the diameter
should be infinite, we express it in terms of the `EMetric.diam` -/
noncomputable def diam (s : Set α) : ℝ :=
  ENNReal.toReal (EMetric.diam s)

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