Graph metric #
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 whenG
is connected. -
Evaluate
nat
vsenat
for the codomain ofdist
, or potentially having an additionaledist
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 #
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) :
@[protected]
theorem
simple_graph.connected.exists_walk_of_dist
{V : Type u_1}
{G : simple_graph V}
(hconn : G.connected)
(u v : V) :
@[simp]
theorem
simple_graph.dist_eq_zero_iff_eq_or_not_reachable
{V : Type u_1}
{G : simple_graph V}
{u v : V} :
@[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) :
@[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) :
@[protected]
theorem
simple_graph.connected.dist_eq_zero_iff
{V : Type u_1}
{G : simple_graph V}
(hconn : G.connected)
{u v : 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) :
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) :
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} :