diam_eq_zero

Mathlib.Combinatorics.SimpleGraph.Diam

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

← MathLib Explorer

English

Diam = 0 iff ediam = ⊤.

Русский

Diam = 0 тогда и только тогда, когда ediam = ⊤.

LaTeX

$$$$ G.diam = 0 \\iff G.ediam = \\top $$$$

Lean4

@[simp]
theorem diam_eq_zero : G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α := by
  rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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