Commit 2024-03-19 23:05 69fd837a

refactor: single-edge graph (#9736) From https://github.com/leanprover-community/mathlib4/pull/9267#discussion_r1451605191:

I would prefer we use lattice operations for adding edges. The idea is to make constructor SimpleGraph.edge (v w : V) : SimpleGraph V that creates a graph with a single edge between v and w if they're not equal (and no edge if they are), and then G.addEdge v w would instead be G ⊔ edge v w. This is more versatile, though perhaps lemmas such as addEdge_of_adj are a bit more brittle to apply.