Multigraphs

Shared graph-theoretic infrastructure reused across papers (e.g. multigraphs, usage matrices) that isn't already in Mathlib. Mathlib's SimpleGraph doesn't allow parallel edges or loops, so multigraphs need their own structure.

structure Multigraph (V : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A multigraph on vertex type V with edge type E: edges are first-class objects (so parallel edges are distinct elements of E), each mapped to its unordered pair of endpoints. A loop is an edge e with endpoints e a diagonal element of Sym2 V.

• endpoints : E → Sym2 V

def Multigraph.toSimpleGraph {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (F : Set E) : SimpleGraph V

The simple graph obtained from a set of edges by forgetting multiplicities, loops, and edge identities, remembering only which pairs of vertices are joined by some edge in F.

Equations

• G.toSimpleGraph F = SimpleGraph.fromEdgeSet (G.endpoints '' F)

theorem Multigraph.toSimpleGraph_support_finite {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {F : Set E} (hF : F.Finite) : (G.toSimpleGraph F).support.Finite

If F is a finite set of edges, then the support of the simple graph on F is finite.

def Multigraph.IsForest {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (F : Set E) : Prop

A set of edges F is a forest if it has no loops, no two edges of F share the same endpoints (parallel edges would form a 2-cycle), and the underlying simple graph on F is acyclic.

Equations

• G.IsForest F = ((∀ e ∈ F, ¬(G.endpoints e).IsDiag) ∧ Set.InjOn G.endpoints F ∧ (G.toSimpleGraph F).IsAcyclic)

def Multigraph.IsSpanningTree {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (T : Set E) : Prop

A set of edges T is a spanning tree if it is a forest whose underlying simple graph is connected, i.e. it touches and joins every vertex of V.

Equations

• G.IsSpanningTree T = (G.IsForest T ∧ (G.toSimpleGraph T).Connected)

theorem Multigraph.IsForest.subset {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {F F' : Set E} (hF : G.IsForest F) (h : F' ⊆ F) : G.IsForest F'

If F is a forest and F' is a subset of F, then F' is also a forest.

theorem Multigraph.IsForest.insert_of_not_reachable {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {F : Set E} (hF : G.IsForest F) {e : E} {u v : V} (heF : e ∉ F) (huv : G.endpoints e = s(u, v)) (hne : u ≠ v) (hreach : ¬(G.toSimpleGraph F).Reachable u v) : G.IsForest (insert e F)

If F is a forest and e={u,v} is an edge not in F with the property that u and v are not reachable in the graph induced by F, then F ∪ {e} is also a forest.

noncomputable def Multigraph.numComponents {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (F : Set E) (S : Set V) : ℕ

The number of connected components of the simple graph on edge set F that meet the vertex set S. Counted as the number of distinct ConnectedComponents hit by S, so a vertex of S untouched by any edge of F contributes its own singleton component.

Equations

• G.numComponents F S = ((G.toSimpleGraph F).connectedComponentMk '' S).ncard

theorem Multigraph.numComponents_pos {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {F : Set E} {S : Set V} (hS : S.Finite) (hSne : S.Nonempty) : 0 < G.numComponents F S

A nonempty, finite vertex set always splits into at least one component.

theorem Multigraph.IsForest.ncard_add_numComponents {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {F : Set E} (hF : G.IsForest F) (hFfin : F.Finite) {S : Set V} (hS : S.Finite) (hFS : (G.toSimpleGraph F).support ⊆ S) : F.ncard + G.numComponents F S = S.ncard

Rank–nullity for forests: a finite forest's edge count equals the number of vertices it touches (or any finite vertex set S containing them) minus the number of components those vertices fall into. This is the key counting fact behind the augmentation property of the cycle matroid (GraphicMatroid): it lets us compare the edge counts of two forests component-by-component.

theorem Multigraph.IsForest.ncard_lt_of_nonempty {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {F : Set E} (hF : G.IsForest F) (hFfin : F.Finite) {S : Set V} (hS : S.Finite) (hSne : S.Nonempty) (hFS : (G.toSimpleGraph F).support ⊆ S) : F.ncard < S.ncard

A finite forest restricted to a finite vertex set S has strictly fewer edges than S has vertices, as long as S is nonempty. The forest need not touch all of S, nor be connected; this is the inequality used for the "smaller" side of the augmentation argument, while IsForest.ncard_add_numComponents gives the exact count needed for the "larger" (already-spanning) side.