Commit 2024-03-19 23:05 69fd837a
View on Github →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 betweenv
andw
if they're not equal (and no edge if they are), and thenG.addEdge v w
would instead beG ⊔ edge v w
. This is more versatile, though perhaps lemmas such asaddEdge_of_adj
are a bit more brittle to apply.