Documentation

Mathlib.Combinatorics.SimpleGraph.Metric

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 #

Todo #

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.

Instances For
    theorem SimpleGraph.dist_le {V : Type u_1} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) :
    theorem SimpleGraph.dist_self {V : Type u_1} {G : SimpleGraph V} {v : V} :
    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) :
    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) :
    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) :
    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} :
    theorem SimpleGraph.dist_comm {V : Type u_1} {G : SimpleGraph V} {u : V} {v : V} :