ediam_bot

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

For a nontrivial vertex set, the bottom graph has extended diameter top, i.e., ediam of the bottom graph is ⊤.

Русский

Для ненулевого множества вершин нижний граф имеет ediam = ⊤.

LaTeX

$$$$ (\\perp : SimpleGraph \\alpha).ediam = \\top $$$$

Lean4

@[simp]
theorem ediam_bot [Nontrivial α] : (⊥ : SimpleGraph α).ediam = ⊤ :=
  ediam_eq_top_of_not_connected not_connected_bot

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

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

Разделы

Аффилиация

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