theorem SimpleGraph.diam_eq_zero_of_subsingleton {α : Type u_1} {G : SimpleGraph α} [Subsingleton α] : G.diam = 0

The diameter is the greatest distance between any two vertices. If the graph is disconnected, this will be 0.

theorem SimpleGraph.nontrivial_of_diam_ne_zero' {α : Type u_1} {G : SimpleGraph α} (h : G.diam ≠ 0) : Nontrivial α