ediam_eq_zero_iff_subsingleton

Mathlib.Combinatorics.SimpleGraph.Diam

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

← MathLib Explorer

English

The ediam of G equals 0 if and only if α is subsingleton.

Русский

ediam(G) = 0 эквивалентно тому, что α является одиночным типом.

LaTeX

$$$ G.ediam = 0 \\iff Subsingleton\\alpha $$$

Lean4

@[simp]
theorem ediam_eq_zero_iff_subsingleton : G.ediam = 0 ↔ Subsingleton α :=
  ⟨subsingleton_of_ediam_eq_zero, fun _ ↦ ediam_eq_zero_of_subsingleton⟩

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

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

Разделы

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

Аффилиация

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