Proof of `Simple-graph representation of a simple multigraph`
groundedproofs/Lax683916Proofs/MultigraphRepresentation.lean · lax-683916
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The representing graph has the actual vertices of the multigraph as its vertex type and joins two vertices exactly when the multigraph does.
Proof strategy
Use mathlib's . Every multigraph edge is sent to its unordered pair of endpoints. Looplessness makes this pair an edge of the simple graph; simplicity makes the map injective; and the definition of adjacency makes it surjective. The identity vertex equivalence and this edge equivalence preserve incidence.
Attribution
Direct completion of the correspondence described in .