dist_le_diam

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

If ediam is finite, then for any vertices u,v we have dist(u,v) ≤ diam(G).

Русский

Если ediam конечен, то для любых вершин u,v расстояние между ними не превосходит diam(G).

LaTeX

$$$$ G.ediam \\neq \\top \\Rightarrow \\forall u,v,\\ G.dist(u,v) \\le G.diam $$$$

Lean4

theorem dist_le_diam (h : G.ediam ≠ ⊤) {u v : α} : G.dist u v ≤ G.diam :=
  ENat.toNat_le_toNat edist_le_ediam h

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

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

Разделы

Аффилиация

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