exists_eccent_eq_ediam_of_finite

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

If α is Nonempty and Finite, there exists u with eccent(u) = ediam.

Русский

Если α непустой и конечно, существует вершина u такая, что eccent(u) = ediam.

LaTeX

$$$ [Nonempty \\alpha] [Finite \\alpha] \\Rightarrow \\exists u, G.eccent u = G.ediam $$$

Lean4

theorem exists_eccent_eq_ediam_of_finite [Nonempty α] [Finite α] : ∃ u, G.eccent u = G.ediam :=
  exists_eq_ciSup_of_finite

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

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

Разделы

Аффилиация

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