SimpleGraph facts #
General SimpleGraph facts that supplement Mathlib but aren't already there.
theorem
SimpleGraph.reachable_le_of_adj_le
{V : Type u_1}
{G : SimpleGraph V}
{R : V → V → Prop}
(hRefl : ∀ (x : V), R x x)
(hTrans : ∀ (x y z : V), R x y → R y z → R x z)
(hAdj : ∀ (x y : V), G.Adj x y → R x y)
(x y : V)
:
G.Reachable x y → R x y
Reachable is the smallest equivalence relation containing Adj: any equivalence
relation that relates every adjacent pair also relates every reachable pair.