mathlib3 documentation

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 #

Todo #

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