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 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
.
Instances For
theorem
SimpleGraph.Reachable.exists_walk_of_dist
{V : Type u_1}
{G : SimpleGraph V}
{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 : SimpleGraph V}
(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 : SimpleGraph V}
{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 : SimpleGraph V}
{u : V}
{v : V}
:
theorem
SimpleGraph.Reachable.dist_eq_zero_iff
{V : Type u_1}
{G : SimpleGraph V}
{u : V}
{v : V}
(hr : G.Reachable u v)
:
theorem
SimpleGraph.Reachable.pos_dist_of_ne
{V : Type u_1}
{G : SimpleGraph V}
{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 : SimpleGraph V}
(hconn : G.Connected)
{u : V}
{v : V}
:
theorem
SimpleGraph.Connected.pos_dist_of_ne
{V : Type u_1}
{G : SimpleGraph V}
{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 : SimpleGraph V}
{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 : SimpleGraph V}
{u : V}
{v : V}
(h : 0 < G.dist u v)
:
Set.univ.Nonempty
theorem
SimpleGraph.Connected.dist_triangle
{V : Type u_1}
{G : SimpleGraph V}
(hconn : G.Connected)
{u : V}
{v : V}
{w : V}
:
theorem
SimpleGraph.dist_comm
{V : Type u_1}
{G : SimpleGraph V}
{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 : SimpleGraph V}
{u : V}
{v : V}
:
theorem
SimpleGraph.Reachable.of_dist_ne_zero
{V : Type u_1}
{G : SimpleGraph V}
{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 : SimpleGraph V}
{u : V}
{v : V}
(h : G.dist u v ≠ 0)
:
∃ (p : G.Walk u v), p.length = G.dist u v
theorem
SimpleGraph.Walk.isPath_of_length_eq_dist
{V : Type u_1}
{G : SimpleGraph V}
{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 : SimpleGraph V}
{u : V}
{v : V}
(hr : G.Reachable u v)
:
theorem
SimpleGraph.Connected.exists_path_of_dist
{V : Type u_1}
{G : SimpleGraph V}
(hconn : G.Connected)
(u : V)
(v : V)
: