English
Let G be a finite simple graph on a nonempty vertex set. Then G is connected if and only if its extended diameter ediam is not the top element.
Русский
Пусть G – конечный простой граф на ненулевом множестве вершин. Тогда G связен тогда и только тогда, когда ediam(G) не равна верхнему пределу.
LaTeX
$$$$ G.Connected \\iff G.ediam \\neq \\top $$$$
Lean4
/-- In a finite graph with nontrivial vertex set, the graph is connected
if and only if the extended diameter is not `⊤`.
See `connected_of_ediam_ne_top` for one of the implications without
the finiteness assumptions -/
theorem connected_iff_ediam_ne_top [Nonempty α] [Finite α] : G.Connected ↔ G.ediam ≠ ⊤ :=
have ⟨u, v, huv⟩ := G.exists_edist_eq_ediam_of_finite
⟨fun h ↦ huv ▸ edist_ne_top_iff_reachable.mpr (h u v), fun h ↦ G.connected_of_ediam_ne_top h⟩
