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.