radius_le_eccent

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

For every vertex u, the radius is at most the eccentricity of u: radius ≤ eccent(u).

Русский

Для каждого вершины u радиус не превышает эксцентриситет u: radius ≤ eccent(u).

LaTeX

$$$$ \\forall u, \\ G.radius \\le G.eccent(u) $$$$

Lean4

theorem radius_le_eccent {u : α} : G.radius ≤ G.eccent u :=
  iInf_le G.eccent u

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

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

Разделы

Аффилиация

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