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.

noncomputable def SimpleGraph.eccent {α : Type u_1} (G : SimpleGraph α) (u : α) : ℕ∞

The eccentricity of a vertex is the greatest distance between it and any other vertex.

Equations

• G.eccent u = ⨆ (v : α), G.edist u v

theorem SimpleGraph.eccent_def {α : Type u_1} {G : SimpleGraph α} : G.eccent = fun (u : α) => ⨆ (v : α), G.edist u v

theorem SimpleGraph.edist_le_eccent {α : Type u_1} {G : SimpleGraph α} {u v : α} : G.edist u v ≤ G.eccent u

theorem SimpleGraph.exists_edist_eq_eccent_of_finite {α : Type u_1} {G : SimpleGraph α} [Finite α] (u : α) : ∃ (v : α), G.edist u v = G.eccent u

theorem SimpleGraph.eccent_eq_top_of_not_connected {α : Type u_1} {G : SimpleGraph α} (h : ¬G.Connected) (u : α) : G.eccent u = ⊤

theorem SimpleGraph.eccent_eq_zero_of_subsingleton {α : Type u_1} {G : SimpleGraph α} [Subsingleton α] (u : α) : G.eccent u = 0

theorem SimpleGraph.eccent_ne_zero {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] (u : α) : G.eccent u ≠ 0

theorem SimpleGraph.eccent_eq_zero_iff {α : Type u_1} {G : SimpleGraph α} (u : α) : G.eccent u = 0 ↔ Subsingleton α

theorem SimpleGraph.eccent_pos_iff {α : Type u_1} {G : SimpleGraph α} (u : α) : 0 < G.eccent u ↔ Nontrivial α

@[simp]

theorem SimpleGraph.eccent_bot {α : Type u_1} [Nontrivial α] (u : α) : ⊥.eccent u = ⊤

@[simp]

theorem SimpleGraph.eccent_top {α : Type u_1} [Nontrivial α] (u : α) : ⊤.eccent u = 1

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 α

noncomputable def SimpleGraph.radius {α : Type u_1} (G : SimpleGraph α) : ℕ∞

The radius of a graph is the minimum eccentricity of its vertices. It's ⊤ for the empty graph.

Equations

• G.radius = ⨅ (u : α), G.eccent u

noncomputable def SimpleGraph.center {α : Type u_1} (G : SimpleGraph α) : Set α

The center of a graph is the set of vertices with minimum eccentricity.

Equations

• G.center = {u : α | G.eccent u = G.radius}

theorem SimpleGraph.center_def {α : Type u_1} {G : SimpleGraph α} : G.center = {u : α | G.eccent u = G.radius}

theorem SimpleGraph.radius_le_eccent {α : Type u_1} {G : SimpleGraph α} {u : α} : G.radius ≤ G.eccent u

theorem SimpleGraph.exists_eccent_eq_radius_of_finite {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α] : ∃ (u : α), G.eccent u = G.radius

theorem SimpleGraph.center_nonempty_of_finite {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α] : G.center.Nonempty