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 #
Provide an additional computable version of
G is connected.
enat for the codomain of
dist, or potentially
having an additional
edist when the objects under consideration are
When directed graphs exist, a directed notion of distance,
graph metric, distance
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