center_nonempty

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

If α is nonempty, the center of G is nonempty.

Русский

Если множество вершин непусто, центр графа непуст.

LaTeX

$$$$ [\mathrmNonempty(\alpha)] \Rightarrow G.\mathrm{center} \neq \varnothing. $$$$

Lean4

theorem center_nonempty [Nonempty α] : G.center.Nonempty :=
  exists_eccent_eq_radius

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

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

Разделы

Аффилиация

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