ediam_ne_zero_iff_nontrivial

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

For any G on α, ediam ≠ 0 if and only if α is nontrivial.

Русский

Для любого графа G над α ediam ≠ 0 тогда и только тогда, когда α не тривиален.

LaTeX

$$$ G.ediam \\neq 0 \\iff Nontrivial\\alpha $$$

Lean4

theorem ediam_ne_zero_iff_nontrivial : G.ediam ≠ 0 ↔ Nontrivial α :=
  ⟨nontrivial_of_ediam_ne_zero, fun _ ↦ ediam_ne_zero⟩

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

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

Разделы

Аффилиация

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