Commit 2025-05-14 23:43 d6c3a2d2

View on Github →

feat(Combinatorics): multigraphs (#24122) This PR defines multigraphs via a structure Graph a b consisting of a vertex set, an edge set, and a 'binary incidence' predicate describing which edges are incident with which vertices. The definition uses the same 'embedded set' design as Matroid: the vertex and edge sets are modelled as Sets rather than types. We give basic API for incidence, adjacency and extensionality. Zulip discussion.

Estimated changes

added theorem Graph.Adj.left_mem
added theorem Graph.Adj.right_mem
added def Graph.Adj
added theorem Graph.Inc.edge_mem
added theorem Graph.Inc.inc_other
added theorem Graph.Inc.isLink_other
added theorem Graph.Inc.vertex_mem
added def Graph.Inc
added theorem Graph.IsLink.adj
added theorem Graph.IsLink.edge_mem
added theorem Graph.IsLink.inc_left
added theorem Graph.IsLink.inc_right
added theorem Graph.IsLink.left_mem
added theorem Graph.IsLink.right_mem
added theorem Graph.IsLoopAt.inc
added def Graph.IsLoopAt
added theorem Graph.IsNonloopAt.inc
added theorem Graph.adj_comm
added theorem Graph.ext_inc
added theorem Graph.isLink_comm
added theorem Graph.isLink_iff_inc
added theorem Graph.isLink_self_iff
added theorem Graph.mk_eq_self
added structure Graph