ediam_le_of_edist_le

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

If every pair of vertices has distance at most k, then the diameter is at most k.

Русский

Если для всех вершин пары расстояние ≤ k, то диаметр ≤ k.

LaTeX

$$∀ {u v}, G.edist u v ≤ k → G.ediam ≤ k$$

Lean4

theorem ediam_le_of_edist_le {k : ℕ∞} (h : ∀ u v, G.edist u v ≤ k) : G.ediam ≤ k :=
  iSup₂_le h

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

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

Разделы

Аффилиация

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