Documentation

Mathlib.Combinatorics.SimpleGraph.Diam

Diameter of a simple graph #

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

Main definitions #

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
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 : α) :
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 : α) :
theorem SimpleGraph.eccent_pos_iff {α : Type u_1} {G : SimpleGraph α} (u : α) :
@[simp]
theorem SimpleGraph.eccent_bot {α : Type u_1} [Nontrivial α] (u : α) :
@[simp]
theorem SimpleGraph.eccent_top {α : Type u_1} [Nontrivial α] (u : α) :
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
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 : α} :
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) :
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_ne_zero {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] :
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

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') :
@[simp]
@[simp]
theorem SimpleGraph.ediam_top {α : Type u_1} [Nontrivial α] :
@[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
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.exists_dist_eq_diam {α : Type u_1} {G : SimpleGraph α} [Nonempty α] :
∃ (u : α) (v : α), G.dist u v = G.diam
theorem SimpleGraph.diam_anti_of_ediam_ne_top {α : Type u_1} {G G' : SimpleGraph α} (h : G G') (hn : G.ediam ) :
@[simp]
theorem SimpleGraph.diam_bot {α : Type u_1} :
@[simp]
theorem SimpleGraph.diam_top {α : Type u_1} [Nontrivial α] :
@[simp]
theorem SimpleGraph.diam_eq_zero {α : Type u_1} {G : SimpleGraph α} :
@[simp]
theorem SimpleGraph.diam_eq_one {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] :
G.diam = 1 G =

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
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 : α} :
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_ediam_iff {α : Type u_1} {G : SimpleGraph α} [Nonempty α] :
G.radius = G.ediam ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
@[simp]
@[simp]
theorem SimpleGraph.radius_top {α : Type u_1} [Nontrivial α] :
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
theorem SimpleGraph.mem_center_iff {α : Type u_1} {G : SimpleGraph α} (u : α) :