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 #

source

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

G.dist u v = has_Inf.Inf (set.range simple_graph.walk.length)

source

@[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

source

@[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

source

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

source

@[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

source

theorem simple_graph.dist_self {V : Type u_1} {G : simple_graph V} {v : V} :

G.dist v v = 0

source

@[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

source

@[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

source

@[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

source

@[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

source

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

source

theorem simple_graph.nonempty_of_pos_dist {V : Type u_1} {G : simple_graph V} {u v : V} (h : 0 < G.dist u v) :

set.univ.nonempty

source

@[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

source

theorem simple_graph.dist_comm {V : Type u_1} {G : simple_graph V} {u v : V} :

G.dist u v = G.dist v u