Bridges and forests of multigraphs

Mathlib defines a bridge of a multigraph G : Graph α β as an edge e forming a singleton edge cut, Graph.IsBridge. This file characterizes bridges through edge-labelled walks:

• Graph.IsLink.isBridge_iff_not_reachable_deleteEdges: an edge joining x and y is a bridge exactly when x and y are not reachable from each other once the edge is deleted.
• Graph.isBridge_iff_exists_not_reachable_deleteEdges: the same criterion with the ends of the edge quantified existentially.
• Graph.IsLink.isBridge_iff_forall_walk_mem_edges: equivalently, every walk between the ends of the edge traverses it.
• Graph.isBridge_iff_forall_cycle_notMem: an actual edge is a bridge exactly when it lies on no cycle.

Consequently loops are never bridges, and neither is an edge having a distinct parallel edge.

Deleting an edge joining x and y affects only the connected component containing them: Graph.IsLink.reachable_iff_reachable_deleteEdges_or shows that this component splits into the components of x and of y in the deletion, which are distinct exactly when the edge is a bridge, and Graph.IsLink.reachable_deleteEdges_iff_of_not_reachable that reachability elsewhere is unchanged. Counting components, Graph.isBridge_iff_componentCount_deleteEdges_eq_add_one shows that, when there are finitely many components, an edge is a bridge exactly when deleting it increases the number of connected components by one; deleting any other edge leaves the number unchanged (Graph.componentCount_deleteEdges_of_not_isBridge). Collecting the bridges into Graph.bridgeSet, Graph.componentCount_deleteEdges_of_subset_bridgeSet_of_finite shows that, with finitely many components, deleting a finite set of bridges adds one component per deleted bridge. With finitely many actual vertices, G has finitely many bridges (Graph.finite_bridgeSet) and deleting all of them leaves exactly G.componentCount + G.bridgeSet.ncard components (Graph.componentCount_deleteEdges_bridgeSet). Deleting every bridge leaves a graph without bridges (Graph.not_isBridge_deleteEdges_bridgeSet).

A multigraph is a forest, Graph.IsForest, when it has no cycles; since loops and pairs of parallel edges are cycles of multigraphs, a forest has neither. Graph.isForest_iff_forall_isBridge shows that a multigraph is a forest exactly when every actual edge is a bridge. In a forest, a walk is a path exactly when it is a trail (Graph.IsForest.isPath_iff_isTrail). Only the component counts assume finiteness: of the components when deleting one bridge or finitely many bridges, and of the actual vertices when deleting all bridges; the other statements need no finiteness assumptions.

The statements follow the corresponding results for simple graphs in Mathlib, SimpleGraph.isBridge_iff, SimpleGraph.isBridge_iff_forall_walk_mem_edges, SimpleGraph.isBridge_iff_forall_cycle_notMem, SimpleGraph.IsBridge.notMem_edges_of_isCycle, SimpleGraph.isAcyclic_iff_forall_isBridge, SimpleGraph.IsAcyclic.isPath_iff_isTrail, and SimpleGraph.IsAcyclic.anti, adapted to multigraphs whose walks record edge identities. The proof of Graph.isForest_iff_forall_isBridge is adapted from Mathlib's proof of SimpleGraph.isAcyclic_iff_forall_isBridge.

Bridges and deletion

theorem Graph.IsBridge.not_reachable_deleteEdges {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y : α} (he : G.IsBridge e) (h : G.IsLink e x y) : ¬(G.deleteEdges {e}).Reachable x y

The ends of a link of a bridge are not reachable from each other once the bridge is deleted.

theorem Graph.IsLink.isBridge_iff_not_reachable_deleteEdges {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y : α} (h : G.IsLink e x y) : G.IsBridge e ↔ ¬(G.deleteEdges {e}).Reachable x y

An edge joining x and y is a bridge exactly when deleting it leaves y unreachable from x.

theorem Graph.isBridge_iff_exists_not_reachable_deleteEdges {α : Type u} {β : Type v} {G : Graph α β} {e : β} : G.IsBridge e ↔ ∃ (x : α) (y : α), G.IsLink e x y ∧ ¬(G.deleteEdges {e}).Reachable x y

An edge is a bridge exactly when it links two vertices that are not reachable from each other once it is deleted.

theorem Graph.IsLink.isBridge_iff_forall_walk_mem_edges {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y : α} (h : G.IsLink e x y) : G.IsBridge e ↔ ∀ (p : G.Walk x y), e ∈ p.edges

An edge joining x and y is a bridge exactly when every walk from x to y traverses it.

theorem Graph.IsLoopAt.not_isBridge {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x : α} (h : G.IsLoopAt e x) : ¬G.IsBridge e

A loop is never a bridge.

theorem Graph.IsLink.not_isBridge_of_isLink_of_ne {α : Type u} {β : Type v} {G : Graph α β} {e f : β} {x y : α} (he : G.IsLink e x y) (hf : G.IsLink f x y) (hfe : f ≠ e) : ¬G.IsBridge e

An edge with a distinct parallel edge is not a bridge.

def Graph.bridgeSet {α : Type u} {β : Type v} (G : Graph α β) : Set β

The set of bridges of G.

@[simp]

theorem Graph.mem_bridgeSet {α : Type u} {β : Type v} {G : Graph α β} {e : β} : e ∈ G.bridgeSet ↔ G.IsBridge e

theorem Graph.bridgeSet_subset_edgeSet {α : Type u} {β : Type v} (G : Graph α β) : G.bridgeSet ⊆ G.edgeSet

Every bridge is an actual edge.

theorem Graph.IsLink.reachable_deleteEdges_bridgeSet {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y : α} (h : G.IsLink e x y) (he : ¬G.IsBridge e) : (G.deleteEdges G.bridgeSet).Reachable x y

The ends of an edge that is not a bridge remain reachable from each other after deleting all bridges.

Bridges and connected components

theorem Graph.reachable_deleteEdges_iff_of_not_isBridge {α : Type u} {β : Type v} {G : Graph α β} {e : β} {u v : α} (he : ¬G.IsBridge e) : (G.deleteEdges {e}).Reachable u v ↔ G.Reachable u v

Deleting an edge that is not a bridge does not change reachability.

theorem Graph.componentCount_deleteEdges_of_not_isBridge {α : Type u} {β : Type v} {G : Graph α β} {e : β} (he : ¬G.IsBridge e) : (G.deleteEdges {e}).componentCount = G.componentCount

Deleting an edge that is not a bridge leaves the number of connected components unchanged.

theorem Graph.IsBridge.componentCount_deleteEdges {α : Type u} {β : Type v} {G : Graph α β} {e : β} [Finite G.ConnectedComponent] (he : G.IsBridge e) : (G.deleteEdges {e}).componentCount = G.componentCount + 1

Deleting a bridge increases the number of connected components by exactly one: the component containing its ends splits into the components of its two ends, and every other component is unchanged.

theorem Graph.isBridge_iff_componentCount_deleteEdges_eq_add_one {α : Type u} {β : Type v} {G : Graph α β} {e : β} [Finite G.ConnectedComponent] : G.IsBridge e ↔ (G.deleteEdges {e}).componentCount = G.componentCount + 1

Bridges by component counts. With finitely many connected components, an edge is a bridge exactly when deleting it increases the number of connected components by one.

theorem Graph.componentCount_deleteEdges_of_subset_bridgeSet_of_finite {α : Type u} {β : Type v} {G : Graph α β} [Finite G.ConnectedComponent] {F : Set β} (hF : F ⊆ G.bridgeSet) (hFfin : F.Finite) : (G.deleteEdges F).componentCount = G.componentCount + F.ncard

With finitely many connected components, deleting a finite set of bridges increases the number of connected components by the number of deleted bridges.

theorem Graph.finite_bridgeSet {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] : G.bridgeSet.Finite

A multigraph with finitely many actual vertices has finitely many bridges.

theorem Graph.componentCount_deleteEdges_of_subset_bridgeSet {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] {F : Set β} (hF : F ⊆ G.bridgeSet) : (G.deleteEdges F).componentCount = G.componentCount + F.ncard

With finitely many actual vertices, deleting a set of bridges increases the number of connected components by the number of deleted bridges.

theorem Graph.componentCount_deleteEdges_bridgeSet {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.vertexSet] : (G.deleteEdges G.bridgeSet).componentCount = G.componentCount + G.bridgeSet.ncard

Counting bridges. With finitely many actual vertices, deleting all bridges leaves as many connected components as G has components and bridges together.

Bridges and cycles

theorem Graph.IsBridge.notMem_edges_of_isCycle {α : Type u} {β : Type v} {G : Graph α β} {e : β} {u : α} (he : G.IsBridge e) {p : G.Walk u u} (hp : p.IsCycle) : e ∉ p.edges

A bridge lies on no cycle.

theorem Graph.isBridge_iff_forall_cycle_notMem {α : Type u} {β : Type v} {G : Graph α β} {e : β} (he : e ∈ G.edgeSet) : G.IsBridge e ↔ ∀ ⦃u : α⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges

An actual edge is a bridge exactly when it lies on no cycle.

theorem Graph.Walk.IsCycle.not_isBridge_of_le {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x : α} {K : Graph α β} (hKG : K ≤ G) {p : K.Walk x x} (hp : p.IsCycle) (he : e ∈ p.edges) : ¬G.IsBridge e

An edge on a cycle in a subgraph is not a bridge in the containing graph.

theorem Graph.Walk.IsCycle.not_isBridge_walkGraph {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} (hp : p.IsCycle) (e : β) : ¬(G.walkGraph p).IsBridge e

No edge of the graph traced by a cycle is a bridge.

theorem Graph.not_isBridge_deleteEdges_bridgeSet {α : Type u} {β : Type v} (G : Graph α β) (e : β) : ¬(G.deleteEdges G.bridgeSet).IsBridge e

Deleting all bridges leaves a graph without bridges.

Forests

def Graph.IsForest {α : Type u} {β : Type v} (G : Graph α β) : Prop

A multigraph is a forest if it has no cycles. Loops and pairs of distinct parallel edges form cycles, so a forest has neither.

theorem Graph.isForest_def {α : Type u} {β : Type v} {G : Graph α β} : G.IsForest ↔ ∀ ⦃u : α⦄ (p : G.Walk u u), ¬p.IsCycle

theorem Graph.isForest_iff_forall_isBridge {α : Type u} {β : Type v} {G : Graph α β} : G.IsForest ↔ ∀ ⦃e : β⦄, e ∈ G.edgeSet → G.IsBridge e

A multigraph is a forest exactly when every actual edge is a bridge.

theorem Graph.IsForest.isBridge {α : Type u} {β : Type v} {G : Graph α β} {e : β} (hG : G.IsForest) (he : e ∈ G.edgeSet) : G.IsBridge e

Every actual edge of a forest is a bridge.

theorem Graph.IsForest.anti {α : Type u} {β : Type v} {G H : Graph α β} (hHG : H ≤ G) (hG : G.IsForest) : H.IsForest

A subgraph of a forest is a forest.

theorem Graph.IsForest.loopless {α : Type u} {β : Type v} {G : Graph α β} (hG : G.IsForest) : G.Loopless

A forest has no loops.

theorem Graph.IsForest.eq_of_isLink {α : Type u} {β : Type v} {G : Graph α β} {e f : β} {x y : α} (hG : G.IsForest) (he : G.IsLink e x y) (hf : G.IsLink f x y) : f = e

Two edges of a forest joining the same ends are equal.

theorem Graph.IsForest.isPath_iff_isTrail {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (hG : G.IsForest) (p : G.Walk x y) : p.IsPath ↔ p.IsTrail

In a forest, a walk is a path exactly when it traverses no edge identity more than once.

theorem Graph.IsForest.edges_subset_of_isPath {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (hG : G.IsForest) {p : G.Walk x y} (hp : p.IsPath) (q : G.Walk x y) : p.edges ⊆ q.edges

Every walk between the endpoints of a path in a forest traverses every edge of that path.

theorem Graph.IsForest.eq_of_isPath {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (hG : G.IsForest) {p q : G.Walk x y} (hp : p.IsPath) (hq : q.IsPath) : p = q

Two paths in a forest with the same endpoints are equal.

@[simp]

theorem Graph.isForest_noEdge {α : Type u} {β : Type v} (X : Set α) : (noEdge X β).IsForest

A graph with no edges is a forest.

Graphs on two vertices

theorem Graph.isBridge_banana_singleton {α : Type u} {β : Type v} {u w : α} (huw : u ≠ w) (e : β) : (banana u w {e}).IsBridge e

The single edge joining two distinct vertices is a bridge.

theorem Graph.isForest_banana_singleton {α : Type u} {β : Type v} {u w : α} (huw : u ≠ w) (e : β) : (banana u w {e}).IsForest

Two distinct vertices joined by a single edge form a forest.

theorem Graph.not_isBridge_banana {α : Type u} {β : Type v} {e f : β} {u w : α} {F : Set β} (hf : f ∈ F) (hfe : f ≠ e) : ¬(banana u w F).IsBridge e

No edge of a graph on two vertices with several edges is a bridge.