Graph metric

This module defines the SimpleGraph.edist function, which takes pairs of vertices to the length of the shortest walk between them, or ⊤ if they are disconnected. It also defines SimpleGraph.dist which is the ℕ-valued version of SimpleGraph.edist, and SimpleGraph.ball which is the open ball in the graph extended metric.

Main definitions

• SimpleGraph.edist is the graph extended metric.
• SimpleGraph.dist is the graph metric.
• SimpleGraph.ball is the open ball of a given radius around a vertex.

TODO

• Provide an additional computable version of SimpleGraph.dist for when G is connected.

• When directed graphs exist, a directed notion of distance, likely ENat-valued.

Tags

graph metric, distance, ball

Metric

noncomputable def SimpleGraph.edist {V : Type u_1} (G : SimpleGraph V) (u v : V) : ℕ∞

The extended distance between two vertices is the length of the shortest walk between them. It is ⊤ if no such walk exists.

Equations

• G.edist u v = ⨅ (w : G.Walk u v), ↑w.length

theorem SimpleGraph.edist_eq_sInf {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.edist u v = sInf (Set.range fun (w : G.Walk u v) => ↑w.length)

theorem SimpleGraph.Reachable.exists_walk_length_eq_edist {V : Type u_1} {G : SimpleGraph V} {u v : V} (hr : G.Reachable u v) : ∃ (p : G.Walk u v), ↑p.length = G.edist u v

theorem SimpleGraph.Connected.exists_walk_length_eq_edist {V : Type u_1} {G : SimpleGraph V} (hconn : G.Connected) (u v : V) : ∃ (p : G.Walk u v), ↑p.length = G.edist u v

theorem SimpleGraph.edist_le {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : G.edist u v ≤ ↑p.length

theorem SimpleGraph.Walk.edist_le {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : G.edist u v ≤ ↑p.length

Alias of SimpleGraph.edist_le.

@[simp]

theorem SimpleGraph.edist_eq_zero_iff {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.edist u v = 0 ↔ u = v

@[simp]

theorem SimpleGraph.edist_self {V : Type u_1} {G : SimpleGraph V} {v : V} : G.edist v v = 0

theorem SimpleGraph.edist_pos_of_ne {V : Type u_1} {G : SimpleGraph V} {u v : V} (hne : u ≠ v) : 0 < G.edist u v

theorem SimpleGraph.edist_eq_top_of_not_reachable {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : ¬G.Reachable u v) : G.edist u v = ⊤

theorem SimpleGraph.reachable_of_edist_ne_top {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.edist u v ≠ ⊤) : G.Reachable u v

theorem SimpleGraph.exists_walk_of_edist_ne_top {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.edist u v ≠ ⊤) : ∃ (p : G.Walk u v), ↑p.length = G.edist u v

theorem SimpleGraph.edist_triangle {V : Type u_1} {G : SimpleGraph V} {u v w : V} : G.edist u w ≤ G.edist u v + G.edist v w

theorem SimpleGraph.edist_comm {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.edist u v = G.edist v u

theorem SimpleGraph.exists_walk_of_edist_eq_coe {V : Type u_1} {G : SimpleGraph V} {u v : V} {k : ℕ} (h : G.edist u v = ↑k) : ∃ (p : G.Walk u v), p.length = k

theorem SimpleGraph.edist_ne_top_iff_reachable {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.edist u v ≠ ⊤ ↔ G.Reachable u v

@[simp]

theorem SimpleGraph.edist_eq_one_iff_adj {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.edist u v = 1 ↔ G.Adj u v

The extended distance between vertices is equal to 1 if and only if these vertices are adjacent.

theorem SimpleGraph.edist_le_one_iff_adj_or_eq {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v

theorem SimpleGraph.edist_eq_two_iff {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.edist u v = 2 ↔ u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty

theorem SimpleGraph.two_lt_edist_iff {V : Type u_1} {G : SimpleGraph V} {u v : V} : 2 < G.edist u v ↔ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅

theorem SimpleGraph.edist_bot_of_ne {V : Type u_1} {u v : V} (h : u ≠ v) : ⊥.edist u v = ⊤

theorem SimpleGraph.edist_bot {V : Type u_1} {u v : V} [DecidableEq V] : ⊥.edist u v = if u = v then 0 else ⊤

theorem SimpleGraph.edist_top_of_ne {V : Type u_1} {u v : V} (h : u ≠ v) : ⊤.edist u v = 1

theorem SimpleGraph.edist_top {V : Type u_1} {u v : V} [DecidableEq V] : ⊤.edist u v = if u = v then 0 else 1

theorem SimpleGraph.edist_anti {V : Type u_1} {G : SimpleGraph V} {u v : V} {G' : SimpleGraph V} (h : G ≤ G') : G'.edist u v ≤ G.edist u v

Supergraphs have smaller or equal extended distances to their subgraphs.

noncomputable def SimpleGraph.dist {V : Type u_1} (G : SimpleGraph V) (u v : V) : ℕ

The distance between two vertices is the length of the shortest walk between them. If no such walk exists, this uses the junk value of 0.

Equations

• G.dist u v = (G.edist u v).toNat

theorem SimpleGraph.dist_eq_sInf {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.dist u v = sInf (Set.range Walk.length)

theorem SimpleGraph.Reachable.coe_dist_eq_edist {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Reachable u v) : ↑(G.dist u v) = G.edist u v

theorem SimpleGraph.Reachable.exists_walk_length_eq_dist {V : Type u_1} {G : SimpleGraph V} {u v : V} (hr : G.Reachable u v) : ∃ (p : G.Walk u v), p.length = G.dist u v

theorem SimpleGraph.Connected.exists_walk_length_eq_dist {V : Type u_1} {G : SimpleGraph V} (hconn : G.Connected) (u v : V) : ∃ (p : G.Walk u v), p.length = G.dist u v

theorem SimpleGraph.dist_le {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : G.dist u v ≤ p.length

@[simp]

theorem SimpleGraph.dist_eq_zero_iff_eq_or_not_reachable {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v

@[simp]

theorem SimpleGraph.dist_self {V : Type u_1} {G : SimpleGraph V} {v : V} : G.dist v v = 0

theorem SimpleGraph.Reachable.dist_eq_zero_iff {V : Type u_1} {G : SimpleGraph V} {u v : V} (hr : G.Reachable u v) : G.dist u v = 0 ↔ u = v

theorem SimpleGraph.Reachable.pos_dist_of_ne {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Reachable u v) (hne : u ≠ v) : 0 < G.dist u v

theorem SimpleGraph.Reachable.one_lt_dist_of_ne_of_not_adj {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Reachable u v) (hne : u ≠ v) (hnadj : ¬G.Adj u v) : 1 < G.dist u v

theorem SimpleGraph.Connected.dist_eq_zero_iff {V : Type u_1} {G : SimpleGraph V} {u v : V} (hconn : G.Connected) : G.dist u v = 0 ↔ u = v

theorem SimpleGraph.Connected.pos_dist_of_ne {V : Type u_1} {G : SimpleGraph V} {u v : V} (hconn : G.Connected) (hne : u ≠ v) : 0 < G.dist u v

theorem SimpleGraph.Connected.one_lt_dist_of_ne_of_not_adj {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Connected) (hne : u ≠ v) (hnadj : ¬G.Adj u v) : 1 < G.dist u v

theorem SimpleGraph.dist_eq_zero_of_not_reachable {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : ¬G.Reachable u v) : G.dist u v = 0

theorem SimpleGraph.nonempty_of_pos_dist {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : 0 < G.dist u v) : Set.univ.Nonempty

theorem SimpleGraph.Connected.dist_triangle {V : Type u_1} {G : SimpleGraph V} {u v w : V} (hconn : G.Connected) : G.dist u w ≤ G.dist u v + G.dist v w

theorem SimpleGraph.Reachable.dist_triangle_left {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Reachable u v) (w : V) : G.dist u w ≤ G.dist u v + G.dist v w

theorem SimpleGraph.Reachable.dist_triangle_right {V : Type u_1} {G : SimpleGraph V} {v w : V} (h : G.Reachable v w) (u : V) : G.dist u w ≤ G.dist u v + G.dist v w

theorem SimpleGraph.dist_comm {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.dist u v = G.dist v u

theorem SimpleGraph.dist_ne_zero_iff_ne_and_reachable {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v

theorem SimpleGraph.Reachable.of_dist_ne_zero {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.dist u v ≠ 0) : G.Reachable u v

theorem SimpleGraph.exists_walk_of_dist_ne_zero {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.dist u v ≠ 0) : ∃ (p : G.Walk u v), p.length = G.dist u v

@[simp]

theorem SimpleGraph.dist_eq_one_iff_adj {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.dist u v = 1 ↔ G.Adj u v

The distance between vertices is equal to 1 if and only if these vertices are adjacent.

theorem SimpleGraph.Adj.diff_dist_adj {V : Type u_1} {G : SimpleGraph V} {u v w : V} (hadj : G.Adj v w) : G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

@[deprecated SimpleGraph.Adj.diff_dist_adj (since := "2025-12-11")]

theorem SimpleGraph.Connected.diff_dist_adj {V : Type u_1} {G : SimpleGraph V} {u v w : V} : G.Connected → ∀ (hadj : G.Adj v w), G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

theorem SimpleGraph.Walk.isPath_of_length_eq_dist {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : p.length = G.dist u v) : p.IsPath

theorem SimpleGraph.Reachable.exists_path_of_dist {V : Type u_1} {G : SimpleGraph V} {u v : V} (hr : G.Reachable u v) : ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

theorem SimpleGraph.Connected.exists_path_of_dist {V : Type u_1} {G : SimpleGraph V} (hconn : G.Connected) (u v : V) : ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

@[simp]

theorem SimpleGraph.dist_bot {V : Type u_1} {u v : V} : ⊥.dist u v = 0

theorem SimpleGraph.dist_top_of_ne {V : Type u_1} {u v : V} (h : u ≠ v) : ⊤.dist u v = 1

theorem SimpleGraph.dist_top {V : Type u_1} {u v : V} [DecidableEq V] : ⊤.dist u v = if u = v then 0 else 1

theorem SimpleGraph.length_eq_dist_of_subwalk {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h₁ : p₁.length = G.dist u v) (h₂ : p₂.IsSubwalk p₁) : p₂.length = G.dist u' v'

theorem SimpleGraph.Reachable.dist_anti {V : Type u_1} {G : SimpleGraph V} {u v : V} {G' : SimpleGraph V} (h : G ≤ G') (hr : G.Reachable u v) : G'.dist u v ≤ G.dist u v

Supergraphs have smaller or equal distances to their subgraphs.

theorem SimpleGraph.Walk.exists_adj_adj_not_adj_ne {V : Type u_1} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.length = G.dist v w) (hl : 1 < G.dist v w) : ∃ (x : V) (a : V) (b : V), G.Adj x a ∧ G.Adj a b ∧ ¬G.Adj x b ∧ x ≠ b

This bundles and abstracts some facts about the first three vertices of a shortest walk of length at least two: the first and third nodes are different and not connected.

Ball

def SimpleGraph.ball {V : Type u_1} (G : SimpleGraph V) (c : V) (r : ℕ∞) : Set V

The open ball of radius r centered at the vertex c in the graph extended metric.

Equations

• G.ball c r = {v : V | G.edist v c < r}

@[simp]

theorem SimpleGraph.mem_ball {V : Type u_1} {G : SimpleGraph V} {c v : V} {r : ℕ∞} : v ∈ G.ball c r ↔ G.edist v c < r

@[simp]

theorem SimpleGraph.ball_zero {V : Type u_1} {G : SimpleGraph V} {c : V} : G.ball c 0 = ∅

The ball of radius zero is empty.

@[simp]

theorem SimpleGraph.ball_one {V : Type u_1} {G : SimpleGraph V} {c : V} : G.ball c 1 = {c}

The ball of radius one consists of just the center.

@[simp]

theorem SimpleGraph.ball_two {V : Type u_1} {G : SimpleGraph V} {c : V} : G.ball c 2 = insert c (G.neighborSet c)

The ball of radius two consists of the center and its neighbors.

theorem SimpleGraph.ball_top {V : Type u_1} {G : SimpleGraph V} {c : V} : G.ball c ⊤ = (G.connectedComponentMk c).supp

The ball of radius ⊤ is the connected component of the center.

theorem SimpleGraph.mem_ball_top {V : Type u_1} {G : SimpleGraph V} {c v : V} : v ∈ G.ball c ⊤ ↔ G.Reachable v c

A vertex is in the ball of radius ⊤ iff it is reachable from the center.

theorem SimpleGraph.ball_mono {V : Type u_1} {G : SimpleGraph V} {c : V} {r₁ r₂ : ℕ∞} (h : r₁ ≤ r₂) : G.ball c r₁ ⊆ G.ball c r₂

Balls are monotone in the radius.

theorem SimpleGraph.mem_ball_self {V : Type u_1} {G : SimpleGraph V} {c : V} {r : ℕ∞} (hr : 0 < r) : c ∈ G.ball c r

The center vertex belongs to any ball of positive radius.

theorem SimpleGraph.mem_ball_comm {V : Type u_1} {G : SimpleGraph V} {c v : V} {r : ℕ∞} : v ∈ G.ball c r ↔ c ∈ G.ball v r

Ball membership is symmetric in center and point.