diam_pair

Mathlib.Topology.EMetricSpace.Diam

URI: https://scilib.ai/kg/mathlib#EMetric.diam_pair

English

The diameter of the two-point set {x,y} equals the distance edist(x,y).

Русский

Диаметр множества из двух точек {x,y} равен расстоянию edist(x,y).

LaTeX

$$\operatorname{diam}(\{x,y\}) = \operatorname{edist}(x,y)$$

Lean4

theorem diam_pair : diam ({ x, y } : Set α) = edist x y := by
  simp only [iSup_singleton, diam_insert, diam_singleton, ENNReal.max_zero_right]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru