Documentation

Mathlib.Combinatorics.SimpleGraph.Diam

Diameter of a simple graph #

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

Main definitions #

Todo #

source
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
Instances For
    source
    theorem SimpleGraph.ediam_def {α : Type u_1} {G : SimpleGraph α} :
    G.ediam = ⨆ (p : α × α), G.edist p.1 p.2
    source
    theorem SimpleGraph.edist_le_ediam {α : Type u_1} {G : SimpleGraph α} {u : α} {v : α} :
    G.edist u v ≤ G.ediam
    source
    theorem SimpleGraph.ediam_le_of_edist_le {α : Type u_1} {G : SimpleGraph α} {k : ℕ∞} (h : ∀ (u v : α), G.edist u v ≤ k) :
    G.ediam ≤ k
    source
    theorem SimpleGraph.ediam_le_iff {α : Type u_1} {G : SimpleGraph α} {k : ℕ∞} :
    G.ediam ≤ k ↔ ∀ (u v : α), G.edist u v ≤ k
    source
    theorem SimpleGraph.ediam_eq_top {α : Type u_1} {G : SimpleGraph α} :
    G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ (u : α) (v : α), b < G.edist u v
    source
    theorem SimpleGraph.ediam_eq_zero_of_subsingleton {α : Type u_1} {G : SimpleGraph α} [Subsingleton α] :
    G.ediam = 0
    source
    theorem SimpleGraph.nontrivial_of_ediam_ne_zero {α : Type u_1} {G : SimpleGraph α} (h : G.ediam ≠ 0) :
    Nontrivial α
    source
    theorem SimpleGraph.ediam_ne_zero {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] :
    G.ediam ≠ 0
    source
    theorem SimpleGraph.subsingleton_of_ediam_eq_zero {α : Type u_1} {G : SimpleGraph α} (h : G.ediam = 0) :
    Subsingleton α
    source
    theorem SimpleGraph.ediam_ne_zero_iff_nontrivial {α : Type u_1} {G : SimpleGraph α} :
    G.ediam ≠ 0 ↔ Nontrivial α
    source
    @[simp]
    theorem SimpleGraph.ediam_eq_zero_iff_subsingleton {α : Type u_1} {G : SimpleGraph α} :
    G.ediam = 0 ↔ Subsingleton α
    source
    theorem SimpleGraph.ediam_eq_top_of_not_connected {α : Type u_1} {G : SimpleGraph α} [Nonempty α] (h : ¬G.Connected) :
    G.ediam = ⊤
    source
    theorem SimpleGraph.ediam_eq_top_of_not_preconnected {α : Type u_1} {G : SimpleGraph α} (h : ¬G.Preconnected) :
    G.ediam = ⊤
    source
    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
    source
    theorem SimpleGraph.exists_edist_eq_ediam_of_finite {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α] :
    ∃ (u : α) (v : α), G.edist u v = G.ediam
    source
    theorem SimpleGraph.ediam_anti {α : Type u_1} {G : SimpleGraph α} {G' : SimpleGraph α} (h : G ≤ G') :
    G'.ediam ≤ G.ediam
    source
    @[simp]
    theorem SimpleGraph.ediam_bot {α : Type u_1} [Nontrivial α] :
    ⊥.ediam = ⊤
    source
    @[simp]
    theorem SimpleGraph.ediam_top {α : Type u_1} [Nontrivial α] :
    ⊤.ediam = 1
    source
    @[simp]
    theorem SimpleGraph.ediam_eq_one {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] :
    G.ediam = 1 ↔ G = ⊤
    source
    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
    Instances For
      source
      theorem SimpleGraph.diam_def {α : Type u_1} {G : SimpleGraph α} :
      G.diam = (⨆ (p : α × α), G.edist p.1 p.2).toNat
      source
      theorem SimpleGraph.dist_le_diam {α : Type u_1} {G : SimpleGraph α} (h : G.ediam ≠ ⊤) {u : α} {v : α} :
      G.dist u v ≤ G.diam
      source
      theorem SimpleGraph.nontrivial_of_diam_ne_zero {α : Type u_1} {G : SimpleGraph α} (h : G.diam ≠ 0) :
      Nontrivial α
      source
      theorem SimpleGraph.diam_eq_zero_of_not_connected {α : Type u_1} {G : SimpleGraph α} (h : ¬G.Connected) :
      G.diam = 0
      source
      theorem SimpleGraph.diam_eq_zero_of_ediam_eq_top {α : Type u_1} {G : SimpleGraph α} (h : G.ediam = ⊤) :
      G.diam = 0
      source
      theorem SimpleGraph.ediam_ne_top_of_diam_ne_zero {α : Type u_1} {G : SimpleGraph α} (h : G.diam ≠ 0) :
      G.ediam ≠ ⊤
      source
      theorem SimpleGraph.exists_dist_eq_diam {α : Type u_1} {G : SimpleGraph α} [Nonempty α] :
      ∃ (u : α) (v : α), G.dist u v = G.diam
      source
      theorem SimpleGraph.diam_anti_of_ediam_ne_top {α : Type u_1} {G : SimpleGraph α} {G' : SimpleGraph α} (h : G ≤ G') (hn : G.ediam ≠ ⊤) :
      G'.diam ≤ G.diam
      source
      @[simp]
      theorem SimpleGraph.diam_bot {α : Type u_1} :
      ⊥.diam = 0
      source
      @[simp]
      theorem SimpleGraph.diam_top {α : Type u_1} [Nontrivial α] :
      ⊤.diam = 1
      source
      @[simp]
      theorem SimpleGraph.diam_eq_zero {α : Type u_1} {G : SimpleGraph α} :
      G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α
      source
      @[simp]
      theorem SimpleGraph.diam_eq_one {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] :
      G.diam = 1 ↔ G = ⊤