English
The diameter of the three-point set {x,y,z} equals the maximum of the pairwise distances in a specific order: max(max(edist x y, edist x z), edist y z).
Русский
Диаметр множества {x,y,z} равен максимальному из расстояний между парами точек: max(max(edist(x,y), edist(x,z)), edist(y,z)).
LaTeX
$$\operatorname{diam}(\{x,y,z\}) = \max\left( \max\left( \operatorname{edist}(x,y), \operatorname{edist}(x,z)\right), \operatorname{edist}(y,z) \right)$$
Lean4
theorem diam_triple : diam ({ x, y, z } : Set α) = max (max (edist x y) (edist x z)) (edist y z) := by
simp only [diam_insert, iSup_insert, iSup_singleton, diam_singleton, ENNReal.max_zero_right]