diam — Mathlib

English

The diameter of a set s in a pseudoemetric space is the supremum of edist between all pairs of points in s.

Русский

Диаметр множества s в псевдоэмметрическом пространстве равен супремуму edist(x,y) по всем x,y ∈ s.

LaTeX

$$$\\mathrm{diam}(s) = \\sup\\{\\, edist(x,y) : x\\in s, y\\in s \\}$$$

Lean4

/-- The diameter of a set in a pseudoemetric space, named `EMetric.diam` -/
noncomputable def diam (s : Set α) :=
  ⨆ (x ∈ s) (y ∈ s), edist x y

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