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 : SimpleGraph V) (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

• SimpleGraph.dist G u v = sInf (Set.range SimpleGraph.Walk.length)

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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