diam_triple — Mathlib

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]

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