Diameter of a simple graph

This module defines the eccentricity of vertices, the diameter, and the radius of a simple graph.

Main definitions

* `SimpleGraph.eccent`: the eccentricity of a vertex in a simple graph, which is the maximum
  distances between it and the other vertices.
* `SimpleGraph.ediam`: the graph extended diameter, which is the maximum eccentricity.
  It is `ℕ∞`-valued.
* `SimpleGraph.diam`: the graph diameter, an `ℕ`-valued version of `SimpleGraph.ediam`.
* `SimpleGraph.radius`: the graph radius, which is the minimum eccentricity. It is `ℕ∞`-valued.
* `SimpleGraph.center`: the set of vertices with eccentricity equal to the graph's radius.

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 α