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.eq_top_iff_forall_eccent_eq_one {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] : G = ⊤ ↔ ∀ (u : α), G.eccent u = 1

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

The extended diameter is the greatest distance between any two vertices, with the value ⊤ in case the distances are not bounded above, or the graph is not connected.

Equations

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

theorem SimpleGraph.ediam_eq_iSup_iSup_edist {α : Type u_1} {G : SimpleGraph α} : G.ediam = ⨆ (u : α), ⨆ (v : α), G.edist u v

theorem SimpleGraph.ediam_def {α : Type u_1} {G : SimpleGraph α} : G.ediam = ⨆ (p : α × α), G.edist p.1 p.2

theorem SimpleGraph.eccent_le_ediam {α : Type u_1} {G : SimpleGraph α} {u : α} : G.eccent u ≤ G.ediam

theorem SimpleGraph.edist_le_ediam {α : Type u_1} {G : SimpleGraph α} {u v : α} : G.edist u v ≤ G.ediam

theorem SimpleGraph.ediam_le_of_edist_le {α : Type u_1} {G : SimpleGraph α} {k : ℕ∞} (h : ∀ (u v : α), G.edist u v ≤ k) : G.ediam ≤ k

theorem SimpleGraph.ediam_le_iff {α : Type u_1} {G : SimpleGraph α} {k : ℕ∞} : G.ediam ≤ k ↔ ∀ (u v : α), G.edist u v ≤ k

theorem SimpleGraph.ediam_eq_top {α : Type u_1} {G : SimpleGraph α} : G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ (u : α) (v : α), b < G.edist u v

theorem SimpleGraph.ediam_eq_zero_of_subsingleton {α : Type u_1} {G : SimpleGraph α} [Subsingleton α] : G.ediam = 0

theorem SimpleGraph.nontrivial_of_ediam_ne_zero {α : Type u_1} {G : SimpleGraph α} (h : G.ediam ≠ 0) : Nontrivial α

theorem SimpleGraph.ediam_ne_zero {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] : G.ediam ≠ 0

theorem SimpleGraph.subsingleton_of_ediam_eq_zero {α : Type u_1} {G : SimpleGraph α} (h : G.ediam = 0) : Subsingleton α

theorem SimpleGraph.ediam_ne_zero_iff_nontrivial {α : Type u_1} {G : SimpleGraph α} : G.ediam ≠ 0 ↔ Nontrivial α

@[simp]

theorem SimpleGraph.ediam_eq_zero_iff_subsingleton {α : Type u_1} {G : SimpleGraph α} : G.ediam = 0 ↔ Subsingleton α

theorem SimpleGraph.ediam_eq_top_of_not_connected {α : Type u_1} {G : SimpleGraph α} [Nonempty α] (h : ¬G.Connected) : G.ediam = ⊤

theorem SimpleGraph.ediam_eq_top_of_not_preconnected {α : Type u_1} {G : SimpleGraph α} (h : ¬G.Preconnected) : G.ediam = ⊤

theorem SimpleGraph.preconnected_of_ediam_ne_top {α : Type u_1} {G : SimpleGraph α} (h : G.ediam ≠ ⊤) : G.Preconnected

theorem SimpleGraph.connected_of_ediam_ne_top {α : Type u_1} {G : SimpleGraph α} [Nonempty α] (h : G.ediam ≠ ⊤) : G.Connected

theorem SimpleGraph.exists_eccent_eq_ediam_of_ne_top {α : Type u_1} {G : SimpleGraph α} [Nonempty α] (h : G.ediam ≠ ⊤) : ∃ (u : α), G.eccent u = G.ediam

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

theorem SimpleGraph.exists_edist_eq_ediam_of_ne_top {α : Type u_1} {G : SimpleGraph α} [Nonempty α] (h : G.ediam ≠ ⊤) : ∃ (u : α) (v : α), G.edist u v = G.ediam

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

theorem SimpleGraph.connected_iff_ediam_ne_top {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α] : G.Connected ↔ G.ediam ≠ ⊤

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 SimpleGraph.ediam_anti {α : Type u_1} {G G' : SimpleGraph α} (h : G ≤ G') : G'.ediam ≤ G.ediam

@[simp]

theorem SimpleGraph.ediam_bot {α : Type u_1} [Nontrivial α] : ⊥.ediam = ⊤

@[simp]

theorem SimpleGraph.ediam_top {α : Type u_1} [Nontrivial α] : ⊤.ediam = 1

@[simp]

theorem SimpleGraph.ediam_eq_one {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] : G.ediam = 1 ↔ G = ⊤

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

The diameter is the greatest distance between any two vertices, with the value 0 in case the distances are not bounded above, or the graph is not connected.

Equations

• G.diam = G.ediam.toNat

theorem SimpleGraph.diam_def {α : Type u_1} {G : SimpleGraph α} : G.diam = (⨆ (p : α × α), G.edist p.1 p.2).toNat

theorem SimpleGraph.dist_le_diam {α : Type u_1} {G : SimpleGraph α} (h : G.ediam ≠ ⊤) {u v : α} : G.dist u v ≤ G.diam

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

theorem SimpleGraph.diam_eq_zero_of_not_connected {α : Type u_1} {G : SimpleGraph α} (h : ¬G.Connected) : G.diam = 0

theorem SimpleGraph.diam_eq_zero_of_ediam_eq_top {α : Type u_1} {G : SimpleGraph α} (h : G.ediam = ⊤) : G.diam = 0

theorem SimpleGraph.ediam_ne_top_of_diam_ne_zero {α : Type u_1} {G : SimpleGraph α} (h : G.diam ≠ 0) : G.ediam ≠ ⊤

theorem SimpleGraph.exists_dist_eq_diam {α : Type u_1} {G : SimpleGraph α} [Nonempty α] : ∃ (u : α) (v : α), G.dist u v = G.diam

theorem SimpleGraph.diam_ne_zero_of_ediam_ne_top {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] (h : G.ediam ≠ ⊤) : G.diam ≠ 0

theorem SimpleGraph.diam_anti_of_ediam_ne_top {α : Type u_1} {G G' : SimpleGraph α} (h : G ≤ G') (hn : G.ediam ≠ ⊤) : G'.diam ≤ G.diam

@[simp]

theorem SimpleGraph.diam_bot {α : Type u_1} : ⊥.diam = 0

@[simp]

theorem SimpleGraph.diam_top {α : Type u_1} [Nontrivial α] : ⊤.diam = 1

@[simp]

theorem SimpleGraph.diam_eq_zero {α : Type u_1} {G : SimpleGraph α} : G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α

@[simp]

theorem SimpleGraph.diam_eq_one {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] : G.diam = 1 ↔ G = ⊤

theorem SimpleGraph.diam_eq_zero_iff_ediam_eq_top {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] : G.diam = 0 ↔ G.ediam = ⊤

theorem SimpleGraph.connected_iff_diam_ne_zero {α : Type u_1} {G : SimpleGraph α} [Finite α] [Nontrivial α] : G.Connected ↔ G.diam ≠ 0

A finite and nontrivial graph is connected if and only if its diameter is not zero. See also connected_iff_ediam_ne_top for the extended diameter version.

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

The radius of a simple graph is the minimum eccentricity of any vertex.

Equations

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

theorem SimpleGraph.radius_eq_iInf_iSup_edist {α : Type u_1} {G : SimpleGraph α} : G.radius = ⨅ (u : α), ⨆ (v : α), G.edist u v

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

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

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

theorem SimpleGraph.radius_eq_top_of_not_connected {α : Type u_1} {G : SimpleGraph α} (h : ¬G.Connected) : G.radius = ⊤

theorem SimpleGraph.radius_eq_top_of_isEmpty {α : Type u_1} {G : SimpleGraph α} [IsEmpty α] : G.radius = ⊤

theorem SimpleGraph.radius_ne_top_iff {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α] : G.radius ≠ ⊤ ↔ G.Connected

theorem SimpleGraph.radius_ne_zero_of_nontrivial {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] : G.radius ≠ 0

theorem SimpleGraph.radius_eq_zero_iff {α : Type u_1} {G : SimpleGraph α} : G.radius = 0 ↔ Nonempty α ∧ Subsingleton α

theorem SimpleGraph.radius_le_ediam {α : Type u_1} {G : SimpleGraph α} [Nonempty α] : G.radius ≤ G.ediam

theorem SimpleGraph.ediam_le_two_mul_radius {α : Type u_1} {G : SimpleGraph α} [Finite α] : G.ediam ≤ 2 * G.radius

theorem SimpleGraph.radius_eq_ediam_iff {α : Type u_1} {G : SimpleGraph α} [Nonempty α] : G.radius = G.ediam ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e

@[simp]

theorem SimpleGraph.radius_bot {α : Type u_1} [Nontrivial α] : ⊥.radius = ⊤

@[simp]

theorem SimpleGraph.radius_top {α : Type u_1} [Nontrivial α] : ⊤.radius = 1

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

The center of a simple graph is the set of vertices with eccentricity equal to the radius.

Equations

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

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

theorem SimpleGraph.mem_center_iff {α : Type u_1} {G : SimpleGraph α} (u : α) : u ∈ G.center ↔ G.eccent u = G.radius

theorem SimpleGraph.center_eq_univ_iff_radius_eq_ediam {α : Type u_1} {G : SimpleGraph α} [Nonempty α] : G.center = Set.univ ↔ G.radius = G.ediam

theorem SimpleGraph.center_eq_univ_of_subsingleton {α : Type u_1} {G : SimpleGraph α} [Subsingleton α] : G.center = Set.univ

theorem SimpleGraph.center_bot {α : Type u_1} : ⊥.center = Set.univ

theorem SimpleGraph.center_top {α : Type u_1} : ⊤.center = Set.univ