ediam_ne_top_of_diam_ne_zero

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

If diam ≠ 0, then ediam ≠ ⊤.

Русский

Если diam ≠ 0, то ediam ≠ ⊤.

LaTeX

$$$$ G.diam \\neq 0 \\Rightarrow G.ediam \\neq \\top $$$$

Lean4

theorem ediam_ne_top_of_diam_ne_zero (h : G.diam ≠ 0) : G.ediam ≠ ⊤ :=
  mt diam_eq_zero_of_ediam_eq_top h

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

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

Разделы

Аффилиация

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