Path decompositions of disconnected graphs #
Concatenating the decompositions of the connected components preserves their common bag-size bound. No vertex belongs to two component blocks.
theorem
Algebraic.Cutwidth.PathDecomposition.exists_of_components
{W : Type}
[Fintype W]
{H : SimpleGraph W}
{b : ℕ}
(parts :
∀ (C : H.ConnectedComponent), ∃ (D : PathDecomposition C.toSimpleGraph), ∀ (i : Fin D.length), (D.bag i).card ≤ b)
:
Combine component decompositions without increasing any bag's size. The result also covers the empty graph, for which zero bags suffice.