Diameter of a simple graph

This module defines the diameter of a simple graph, which measures the maximum distance between vertices.

Main definitions

• SimpleGraph.ediam is the graph extended diameter.

• SimpleGraph.diam is the graph diameter.

Todo

• Prove that G.egirth ≤ 2 * G.ediam + 1 and G.girth ≤ 2 * G.diam + 1 when the diameter is non-zero.

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 : α), ⨆ (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.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_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 α} [Fintype α] [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.