diam_eq_one

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

Diameter equals one iff the graph is top.

Русский

Диаметр равен единице тогда, когда граф есть верхний.

LaTeX

$$$$ G.diam = 1 \\iff G = \\top $$$$

Lean4

@[simp]
theorem diam_eq_one [Nontrivial α] : G.diam = 1 ↔ G = ⊤ := by
  rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]

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

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

Разделы

Аффилиация

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