# Graph metric #

This module defines the SimpleGraph.dist function, which takes pairs of vertices to the length of the shortest walk between them.

## Main definitions #

• SimpleGraph.dist is the graph metric.

## TODO #

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

• Evaluate Nat vs ENat for the codomain of dist, or potentially having an additional edist when the objects under consideration are disconnected graphs.

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

## Tags #

graph metric, distance

## Metric #

noncomputable def SimpleGraph.dist {V : Type u_1} (G : ) (u : V) (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
Instances For
theorem SimpleGraph.Reachable.exists_walk_of_dist {V : Type u_1} {G : } {u : V} {v : V} (hr : G.Reachable u v) :
∃ (p : G.Walk u v), p.length = G.dist u v
theorem SimpleGraph.Connected.exists_walk_of_dist {V : Type u_1} {G : } (hconn : G.Connected) (u : V) (v : V) :
∃ (p : G.Walk u v), p.length = G.dist u v
theorem SimpleGraph.dist_le {V : Type u_1} {G : } {u : V} {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 : } {u : V} {v : V} :
G.dist u v = 0 u = v ¬G.Reachable u v
theorem SimpleGraph.dist_self {V : Type u_1} {G : } {v : V} :
G.dist v v = 0
theorem SimpleGraph.Reachable.dist_eq_zero_iff {V : Type u_1} {G : } {u : V} {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 : } {u : V} {v : V} (h : G.Reachable u v) (hne : u v) :
0 < G.dist u v
theorem SimpleGraph.Connected.dist_eq_zero_iff {V : Type u_1} {G : } (hconn : G.Connected) {u : V} {v : V} :
G.dist u v = 0 u = v
theorem SimpleGraph.Connected.pos_dist_of_ne {V : Type u_1} {G : } {u : V} {v : V} (hconn : G.Connected) (hne : u v) :
0 < G.dist u v
theorem SimpleGraph.dist_eq_zero_of_not_reachable {V : Type u_1} {G : } {u : V} {v : V} (h : ¬G.Reachable u v) :
G.dist u v = 0
theorem SimpleGraph.nonempty_of_pos_dist {V : Type u_1} {G : } {u : V} {v : V} (h : 0 < G.dist u v) :
Set.univ.Nonempty
theorem SimpleGraph.Connected.dist_triangle {V : Type u_1} {G : } (hconn : G.Connected) {u : V} {v : V} {w : V} :
G.dist u w G.dist u v + G.dist v w
theorem SimpleGraph.dist_comm {V : Type u_1} {G : } {u : V} {v : V} :
G.dist u v = G.dist v u
theorem SimpleGraph.dist_ne_zero_iff_ne_and_reachable {V : Type u_1} {G : } {u : V} {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 : } {u : V} {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 : } {u : V} {v : V} (h : G.dist u v 0) :
∃ (p : G.Walk u v), p.length = G.dist u v
theorem SimpleGraph.dist_eq_one_iff_adj {V : Type u_1} {G : } {u : V} {v : V} :
G.dist u v = 1 G.Adj u v
theorem SimpleGraph.Walk.isPath_of_length_eq_dist {V : Type u_1} {G : } {u : V} {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 : } {u : V} {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 : } (hconn : G.Connected) (u : V) (v : V) :
∃ (p : G.Walk u v), p.IsPath p.length = G.dist u v