diam_eq_sSup

Mathlib.Topology.EMetricSpace.Diam

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

English

The diameter can be expressed as a supremum over pairwise distances via image2 edist.

Русский

Диаметр выражается как супремум расстояний между парами через образ edist.

LaTeX

$$$\\mathrm{diam}(s) = \\mathrm{sSup}(\\mathrm{image2}\\ \\mathrm{edist}\\ s\\ s)$$$

Lean4

theorem diam_eq_sSup (s : Set α) : diam s = sSup (image2 edist s s) :=
  sSup_image2.symm

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

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

Разделы

Аффилиация

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