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.