# mathlib3documentation

combinatorics.simple_graph.metric

# Graph metric #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• simple_graph.dist is the graph metric.

## Todo #

• Provide an additional computable version of simple_graph.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 simple_graph.dist {V : Type u_1} (G : simple_graph 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
@[protected]
theorem simple_graph.reachable.exists_walk_of_dist {V : Type u_1} {G : simple_graph V} {u v : V} (hr : G.reachable u v) :
(p : G.walk u v), p.length = G.dist u v
@[protected]
theorem simple_graph.connected.exists_walk_of_dist {V : Type u_1} {G : simple_graph V} (hconn : G.connected) (u v : V) :
(p : G.walk u v), p.length = G.dist u v
theorem simple_graph.dist_le {V : Type u_1} {G : simple_graph V} {u v : V} (p : G.walk u v) :
G.dist u v p.length
@[simp]
theorem simple_graph.dist_eq_zero_iff_eq_or_not_reachable {V : Type u_1} {G : simple_graph V} {u v : V} :
G.dist u v = 0 u = v ¬G.reachable u v
theorem simple_graph.dist_self {V : Type u_1} {G : simple_graph V} {v : V} :
G.dist v v = 0
@[protected]
theorem simple_graph.reachable.dist_eq_zero_iff {V : Type u_1} {G : simple_graph V} {u v : V} (hr : G.reachable u v) :
G.dist u v = 0 u = v
@[protected]
theorem simple_graph.reachable.pos_dist_of_ne {V : Type u_1} {G : simple_graph V} {u v : V} (h : G.reachable u v) (hne : u v) :
0 < G.dist u v
@[protected]
theorem simple_graph.connected.dist_eq_zero_iff {V : Type u_1} {G : simple_graph V} (hconn : G.connected) {u v : V} :
G.dist u v = 0 u = v
@[protected]
theorem simple_graph.connected.pos_dist_of_ne {V : Type u_1} {G : simple_graph V} {u v : V} (hconn : G.connected) (hne : u v) :
0 < G.dist u v
theorem simple_graph.dist_eq_zero_of_not_reachable {V : Type u_1} {G : simple_graph V} {u v : V} (h : ¬G.reachable u v) :
G.dist u v = 0
theorem simple_graph.nonempty_of_pos_dist {V : Type u_1} {G : simple_graph V} {u v : V} (h : 0 < G.dist u v) :
@[protected]
theorem simple_graph.connected.dist_triangle {V : Type u_1} {G : simple_graph V} (hconn : G.connected) {u v w : V} :
G.dist u w G.dist u v + G.dist v w
theorem simple_graph.dist_comm {V : Type u_1} {G : simple_graph V} {u v : V} :
G.dist u v = G.dist v u