subsingleton_of_ediam_eq_zero

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

If the ediam of G is zero, then the vertex set α is subsingleton.

Русский

Если ediam(G) = 0, то множество вершин α является subsingleton (одиночного типа).

LaTeX

$$$ \\forall {\\alpha} {G:\\text{ SimpleGraph }\\alpha},\\ G.ediam = 0 \\Rightarrow Subsingleton\\alpha$$$

Lean4

theorem subsingleton_of_ediam_eq_zero (h : G.ediam = 0) : Subsingleton α :=
  by
  contrapose! h
  exact ediam_ne_zero

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

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

Разделы

Аффилиация

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