diam_eq_zero_iff_ediam_eq_top — Mathlib

English

For a nontrivial graph G, the diameter is zero if and only if the edge-diameter is top (infinite).

Русский

Для ненулевого графа G диаметр равен нулю тогда и только тогда, когда edge-diameter равно верхней границе (бесконечность).

LaTeX

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

Lean4

theorem diam_eq_zero_iff_ediam_eq_top [Nontrivial α] : G.diam = 0 ↔ G.ediam = ⊤ :=
  by
  rw [← not_iff_not]
  exact ⟨ediam_ne_top_of_diam_ne_zero, diam_ne_zero_of_ediam_ne_top⟩

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