Connected components of multigraphs

A connected component of a multigraph is a minimal nonempty closed subgraph. This formulation retains every loop and parallel-edge identity in a component, while the component partition of the actual vertices agrees with the connected components of the underlying simple graph.

The definitions of Graph.IsConnectedComponentOf and Graph.Connected, together with their elementary order API, follow Peter Nelson and Jun Kwon's Mathlib proposal mathlib4#37861. The comparison with SimpleGraph.ConnectedComponent and the finite component count are developed here.

Main definitions

• Graph.IsConnectedComponentOf H G says that H is a minimal nonempty closed subgraph of G.
• Graph.Connected G says that G is its own connected component.
• Graph.ConnectedComponent G is the type of connected-component subgraphs of G.
• Graph.connectedComponentOf G x hx is the connected component containing the vertex x.
• Graph.connectedComponentEquiv identifies these subgraphs with the connected components of G.toSimpleGraph.
• Graph.componentCount G counts the components via Nat.card, so it is 0 if there are infinitely many; it is exact whenever there are finitely many components.
• Graph.ConnectedComponent.mapOfLE maps native components along a subgraph inclusion.

Component membership is described by the walk-based Graph.Reachable, which agrees with reachability in the underlying simple graph.

Component subgraphs and connectedness

def Graph.IsConnectedComponentOf {α : Type u_1} {β : Type u_2} (H G : Graph α β) : Prop

A connected component of G is a minimal nonempty closed subgraph of G.

theorem Graph.isConnectedComponentOf_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H.IsConnectedComponentOf G ↔ H.IsClosedSubgraph G ∧ H.vertexSet.Nonempty ∧ ∀ ⦃K : Graph α β⦄, K.IsClosedSubgraph G → K.vertexSet.Nonempty → K ≤ H → K = H

A connected component of G is a nonempty closed subgraph of G that contains no smaller nonempty closed subgraph of G.

@[simp]

theorem Graph.IsConnectedComponentOf.isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsConnectedComponentOf G) : H.IsClosedSubgraph G

A connected component is closed in its ambient graph.

theorem Graph.IsConnectedComponentOf.isInducedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsConnectedComponentOf G) : H.IsInducedSubgraph G

A connected component is induced in its ambient graph.

@[simp]

theorem Graph.IsConnectedComponentOf.le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsConnectedComponentOf G) : H ≤ G

A connected component is a subgraph of its ambient graph.

theorem Graph.IsConnectedComponentOf.nonempty {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsConnectedComponentOf G) : H.vertexSet.Nonempty

A connected component has an actual vertex.

theorem Graph.IsConnectedComponentOf.anti_right {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hKH : K ≤ H) (hHG : H ≤ G) (h : K.IsConnectedComponentOf G) : K.IsConnectedComponentOf H

A component of G contained in an intermediate graph is a component of that graph.

def Graph.Connected {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

A multigraph is connected when it is a connected component of itself. In particular, the empty graph is not connected.

theorem Graph.connected_iff_isConnectedComponentOf_self {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Connected ↔ G.IsConnectedComponentOf G

A multigraph is connected exactly when it is a connected component of itself.

theorem Graph.Connected.nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) : G.vertexSet.Nonempty

A connected graph has an actual vertex.

@[simp]

theorem Graph.not_connected_bot {α : Type u_1} {β : Type u_2} : ¬⊥.Connected

The empty graph is not connected.

theorem Graph.connected_iff_forall_closed {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.vertexSet.Nonempty) : G.Connected ↔ ∀ {H : Graph α β}, H.IsClosedSubgraph G → H.vertexSet.Nonempty → H = G

A nonempty graph is connected exactly when it has no proper nonempty closed subgraph.

theorem Graph.connected_iff_forall_closed_ge {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.vertexSet.Nonempty) : G.Connected ↔ ∀ {H : Graph α β}, H.IsClosedSubgraph G → H.vertexSet.Nonempty → G ≤ H

A nonempty graph is connected exactly when every nonempty closed subgraph contains it.

theorem Graph.Connected.ext_of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.IsClosedSubgraph G) (hne : H.vertexSet.Nonempty) (hG : G.Connected) : H = G

A nonempty closed subgraph of a connected graph is the whole graph.

theorem Graph.IsConnectedComponentOf.connected {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsConnectedComponentOf G) : H.Connected

Every connected-component subgraph is connected.

@[reducible, inline]

abbrev Graph.ConnectedComponent {α : Type u_1} {β : Type u_2} (G : Graph α β) : Type (max 0 u_1 u_2)

The connected-component subgraphs of G.

Comparison with the underlying simple graph

def Graph.connectedComponentVertexSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (C : G.toSimpleGraph.ConnectedComponent) : Set α

The actual vertices belonging to a component of the underlying simple graph.

@[simp]

theorem Graph.mem_connectedComponentVertexSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : G.toSimpleGraph.ConnectedComponent} {x : α} : x ∈ G.connectedComponentVertexSet C ↔ ∃ (hx : x ∈ G.vertexSet), ⟨x, hx⟩ ∈ C.supp

A point belongs to the lifted vertex set exactly when it has a proof of membership in the ambient graph whose corresponding actual vertex lies in the simple component.

def Graph.connectedComponentSubgraph {α : Type u_1} {β : Type u_2} (G : Graph α β) (C : G.toSimpleGraph.ConnectedComponent) : Graph α β

The multigraph induced on a component of its underlying simple graph. It retains all loops and all parallel-edge identities whose endpoints lie in the component.

@[simp]

theorem Graph.vertexSet_connectedComponentSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : (G.connectedComponentSubgraph C).vertexSet = G.connectedComponentVertexSet C

@[simp]

theorem Graph.connectedComponentSubgraph_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) (e : β) (x y : α) : (G.connectedComponentSubgraph C).IsLink e x y ↔ G.IsLink e x y ∧ x ∈ G.connectedComponentVertexSet C ∧ y ∈ G.connectedComponentVertexSet C

Links of a component subgraph are precisely the ambient links with both endpoints in its component vertex set.

theorem Graph.edgeSet_connectedComponentSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : (G.connectedComponentSubgraph C).edgeSet = {e : β | ∃ (x : α) (y : α), G.IsLink e x y ∧ x ∈ G.connectedComponentVertexSet C ∧ y ∈ G.connectedComponentVertexSet C}

The edges of a component subgraph are the ambient edges with both endpoints in its component vertex set.

theorem Graph.connectedComponentSubgraph_le {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : G.connectedComponentSubgraph C ≤ G

The component subgraph induced by a simple connected component is a subgraph of the multigraph.

theorem Graph.connectedComponentSubgraph_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : (G.connectedComponentSubgraph C).IsClosedSubgraph G

The component subgraph induced by a simple connected component is closed in the multigraph.

theorem Graph.connectedComponentVertexSet_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : (G.connectedComponentVertexSet C).Nonempty

The component subgraph induced by a simple connected component is nonempty.

theorem Graph.connectedComponentSubgraph_le_of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : G.toSimpleGraph.ConnectedComponent} (hH : H.IsClosedSubgraph G) {x : ↑G.vertexSet} (hxC : x ∈ C.supp) (hxH : ↑x ∈ H.vertexSet) : G.connectedComponentSubgraph C ≤ H

A closed subgraph sharing a vertex with a simple component contains the whole component subgraph.

theorem Graph.connectedComponentSubgraph_isConnectedComponentOf {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : (G.connectedComponentSubgraph C).IsConnectedComponentOf G

Lifting an underlying simple component gives a connected component of the multigraph.

def Graph.ConnectedComponent.ofSimple {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : G.ConnectedComponent

Regard an underlying simple component as a connected-component subgraph.

@[simp]

theorem Graph.ConnectedComponent.coe_ofSimple {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : ↑(ofSimple C) = G.connectedComponentSubgraph C

The subgraph underlying the lifted simple component is its induced component subgraph.

noncomputable def Graph.ConnectedComponent.toSimple {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.ConnectedComponent) : G.toSimpleGraph.ConnectedComponent

The underlying simple component containing a connected-component subgraph.

@[simp]

theorem Graph.ConnectedComponent.ofSimple_toSimple {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.ConnectedComponent) : ofSimple C.toSimple = C

A connected-component subgraph is the induced graph on the support of its underlying simple component.

theorem Graph.ConnectedComponent.mem_supp_toSimple_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.ConnectedComponent) (x : ↑G.vertexSet) : x ∈ C.toSimple.supp ↔ ↑x ∈ (↑C).vertexSet

The support of the underlying simple component is exactly the actual vertex set of the component subgraph.

@[simp]

theorem Graph.ConnectedComponent.connectedComponentMk_eq_toSimple_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.ConnectedComponent) (x : ↑G.vertexSet) : G.toSimpleGraph.connectedComponentMk x = C.toSimple ↔ ↑x ∈ (↑C).vertexSet

A vertex lies in the underlying simple component of a connected-component subgraph exactly when it is a vertex of that subgraph.

@[simp]

theorem Graph.ConnectedComponent.toSimple_ofSimple {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : (ofSimple C).toSimple = C

Passing from an underlying simple component to its component subgraph and back recovers the simple component.

noncomputable def Graph.connectedComponentEquiv {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.ConnectedComponent ≃ G.toSimpleGraph.ConnectedComponent

Connected-component subgraphs are equivalent to connected components of the underlying simple graph.

@[simp]

theorem Graph.connectedComponentEquiv_apply {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.ConnectedComponent) : G.connectedComponentEquiv C = C.toSimple

The component equivalence sends a component subgraph to its underlying simple component.

@[simp]

theorem Graph.connectedComponentEquiv_symm_apply {α : Type u_1} {β : Type u_2} {G : Graph α β} (C : G.toSimpleGraph.ConnectedComponent) : G.connectedComponentEquiv.symm C = ConnectedComponent.ofSimple C

The inverse component equivalence induces the ambient multigraph on a simple component.

theorem Graph.IsConnectedComponentOf.eq_of_mem_of_mem {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hH : H.IsConnectedComponentOf G) (hK : K.IsConnectedComponentOf G) {x : α} (hxH : x ∈ H.vertexSet) (hxK : x ∈ K.vertexSet) : H = K

Two connected components sharing a vertex are equal.

theorem Graph.ConnectedComponent.eq_of_mem_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {C D : G.ConnectedComponent} {x : α} (hxC : x ∈ (↑C).vertexSet) (hxD : x ∈ (↑D).vertexSet) : C = D

Two connected-component subgraphs sharing a vertex are equal.

theorem Graph.toSimpleGraph_connectedComponentMk_eq_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {z w : ↑G.vertexSet} : G.toSimpleGraph.connectedComponentMk z = G.toSimpleGraph.connectedComponentMk w ↔ G.Reachable ↑z ↑w

Two actual vertices have the same simple component exactly when they are reachable from each other.

def Graph.connectedComponentOf {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) (hx : x ∈ G.vertexSet) : G.ConnectedComponent

The connected-component subgraph containing an actual vertex.

@[simp]

theorem Graph.ConnectedComponent.toSimple_connectedComponentOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : (G.connectedComponentOf x hx).toSimple = G.toSimpleGraph.connectedComponentMk ⟨x, hx⟩

The underlying simple component of the component of x is the simple component of x.

@[simp]

theorem Graph.mem_vertexSet_connectedComponentOf_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hx : x ∈ G.vertexSet) : y ∈ (↑(G.connectedComponentOf x hx)).vertexSet ↔ G.Reachable x y

A vertex lies in the component of x exactly when it is reachable from x.

theorem Graph.mem_vertexSet_connectedComponentOf_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : x ∈ (↑(G.connectedComponentOf x hx)).vertexSet

A vertex lies in its own connected component.

@[simp]

theorem Graph.connectedComponentOf_eq_connectedComponentOf_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : G.connectedComponentOf x hx = G.connectedComponentOf y hy ↔ G.Reachable x y

Two vertices have the same connected component exactly when they are reachable from each other.

theorem Graph.ConnectedComponent.eq_connectedComponentOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : G.ConnectedComponent} {x : α} (hx : x ∈ (↑C).vertexSet) : C = G.connectedComponentOf x ⋯

A connected-component subgraph is the component of each of its vertices.

theorem Graph.isConnectedComponentOf_iff_exists_eq_connectedComponentSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H.IsConnectedComponentOf G ↔ ∃ (C : G.toSimpleGraph.ConnectedComponent), H = G.connectedComponentSubgraph C

A subgraph is a connected component exactly when it is induced on a component of the underlying simple graph.

Connectedness and the component count

theorem Graph.connected_iff_toSimpleGraph_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Connected ↔ G.toSimpleGraph.Connected

Multigraph connectedness agrees with connectedness of the underlying simple graph.

theorem Graph.connected_iff_forall_reachable {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Connected ↔ G.vertexSet.Nonempty ∧ ∀ ⦃x y : α⦄, x ∈ G.vertexSet → y ∈ G.vertexSet → G.Reachable x y

A multigraph is connected exactly when it has an actual vertex and any two actual vertices are reachable from each other.

theorem Graph.Connected.reachable {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) {x y : α} (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : G.Reachable x y

Any two actual vertices of a connected multigraph are reachable from each other.

theorem Graph.Walk.connected_walkGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (p : G.Walk x y) : (G.walkGraph p).Connected

The graph traced by a walk is connected.

instance Graph.instFiniteConnectedComponentOfElemVertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} [Finite ↑G.vertexSet] : Finite G.ConnectedComponent

Finitely many actual vertices give finitely many connected-component subgraphs.

noncomputable def Graph.componentCount {α : Type u_1} {β : Type u_2} (G : Graph α β) : ℕ

The number of connected-component subgraphs of G, or 0 if there are infinitely many.

theorem Graph.componentCount_def {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.componentCount = Nat.card G.ConnectedComponent

The component count is the cardinality of the native component-subgraph type.

theorem Graph.componentCount_eq_natCard_toSimpleGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.componentCount = Nat.card G.toSimpleGraph.ConnectedComponent

The component count is the number of connected components of the underlying simple graph.

theorem Graph.componentCount_ofSimpleGraph {α : Type u_1} (H : SimpleGraph α) : (ofSimpleGraph H).componentCount = Nat.card H.ConnectedComponent

The component count of a simple graph regarded as a multigraph is its usual number of connected components.

@[simp]

theorem Graph.componentCount_eq_zero_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} [Finite G.ConnectedComponent] : G.componentCount = 0 ↔ G.vertexSet = ∅

A multigraph with finitely many components has no components exactly when it has no actual vertices.

@[simp]

theorem Graph.componentCount_eq_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.componentCount = 1 ↔ G.Connected

A multigraph has one component exactly when it is connected.

theorem Graph.componentCount_le_ncard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} [Finite ↑G.vertexSet] : G.componentCount ≤ G.vertexSet.ncard

A multigraph with finitely many actual vertices has at most as many components as actual vertices.

Subgraph inclusions

theorem Graph.map_toSimpleGraphHomOfLE_connectedComponentMk_eq_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) {z : ↑H.vertexSet} {w : ↑G.vertexSet} : SimpleGraph.ConnectedComponent.map (toSimpleGraphHomOfLE hHG) (H.toSimpleGraph.connectedComponentMk z) = G.toSimpleGraph.connectedComponentMk w ↔ G.Reachable ↑z ↑w

Along a subgraph inclusion H ≤ G, the simple component of z in H maps to the simple component of w in G exactly when w is reachable from z in G.

theorem Graph.map_toSimpleGraphHomOfLE_connectedComponentMk_eq_map_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) {z w : ↑H.vertexSet} : SimpleGraph.ConnectedComponent.map (toSimpleGraphHomOfLE hHG) (H.toSimpleGraph.connectedComponentMk z) = SimpleGraph.ConnectedComponent.map (toSimpleGraphHomOfLE hHG) (H.toSimpleGraph.connectedComponentMk w) ↔ G.Reachable ↑z ↑w

Along a subgraph inclusion H ≤ G, the simple components in H of z and w have the same image exactly when w is reachable from z in G.

noncomputable def Graph.ConnectedComponent.mapOfLE {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) : H.ConnectedComponent → G.ConnectedComponent

A subgraph inclusion maps each native connected component to the ambient connected component containing it.

@[simp]

theorem Graph.ConnectedComponent.mapOfLE_connectedComponentOf {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) {x : α} (hx : x ∈ H.vertexSet) : mapOfLE hHG (H.connectedComponentOf x hx) = G.connectedComponentOf x ⋯

The component containing a vertex maps along an inclusion to the ambient component containing that vertex.

theorem Graph.ConnectedComponent.mem_vertexSet_mapOfLE {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) (C : H.ConnectedComponent) {x : α} (hx : x ∈ (↑C).vertexSet) : x ∈ (↑(mapOfLE hHG C)).vertexSet

Every vertex of a component remains in the ambient component obtained by mapping along a subgraph inclusion.

theorem Graph.ConnectedComponent.mapOfLE_eq_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) {C : H.ConnectedComponent} {D : G.ConnectedComponent} : mapOfLE hHG C = D ↔ (↑C).vertexSet ⊆ (↑D).vertexSet

A component maps along a subgraph inclusion to exactly the ambient component containing all of its vertices.

theorem Graph.finite_connectedComponent_of_finite_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : Set α) [Finite ↑S] [Finite (G.deleteVerts S).ConnectedComponent] : Finite G.ConnectedComponent

If deleting a finite set of vertices leaves finitely many connected components, then the original graph also has finitely many connected components.

Basic examples

@[simp]

theorem Graph.componentCount_bot {α : Type u_1} {β : Type u_2} : ⊥.componentCount = 0

The empty graph has no connected components.

theorem Graph.connected_of_vertexSet_eq_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : G.vertexSet = {x}) : G.Connected

A graph with a single actual vertex is connected, whatever loops it carries.

theorem Graph.componentCount_eq_one_of_vertexSet_eq_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : G.vertexSet = {x}) : G.componentCount = 1

A graph with a single actual vertex has exactly one component, whatever loops it carries.

@[simp]

theorem Graph.componentCount_noEdge_singleton {α : Type u_1} {β : Type u_2} (x : α) : (noEdge {x} β).componentCount = 1

A single isolated vertex is one connected component.

@[simp]

theorem Graph.componentCount_banana {α : Type u_1} {β : Type u_2} {x y : α} {F : Set β} (hF : F.Nonempty) : (banana x y F).componentCount = 1

Two vertices joined by a nonempty set of edges form one component. When x = y the edges are loops at a single vertex; otherwise they are parallel edges joining x to y.