radius_le_ediam

Mathlib.Combinatorics.SimpleGraph.Diam

URI: https://scilib.ai/kg/mathlib#SimpleGraph.radius_le_ediam

English

The radius is always at most the eccentric diameter.

Русский

Радиус всегда не превосходит эдиям (расстояние между наиболее удалёнными вершинами).

LaTeX

$$$$\forall {\alpha}, \forall G:\mathrm{SimpleGraph}(\alpha), [\mathrmNonempty(\alpha)]: G.radius \le G.ediam. $$$$

Lean4

theorem radius_le_ediam [Nonempty α] : G.radius ≤ G.ediam :=
  iInf_le_iSup

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

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

Разделы

Аффилиация

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