Joining decompositions of connected components #
Order the components arbitrarily, put each component's bags in a consecutive
block, and enumerate that finite linear order by Fin. No bag grows.
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_of_ordered_bags
{W : Type}
{H : SimpleGraph W}
{I : Type}
[Fintype I]
[LinearOrder I]
(bag : I → Finset W)
(vertices : ∀ (w : W), ∃ (i : I), w ∈ bag i)
(edges : ∀ (u v : W), H.Adj u v → ∃ (i : I), u ∈ bag i ∧ v ∈ bag i)
(intervals : ∀ (w : W) (i j k : I), i ≤ j → j ≤ k → w ∈ bag i → w ∈ bag k → w ∈ bag j)
{b : ℕ}
(bound : ∀ (i : I), (bag i).card ≤ b)
:
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.exists_of_components
{W : Type}
{H : SimpleGraph W}
[Fintype W]
{b : ℕ}
(parts :
∀ (C : H.ConnectedComponent), ∃ (D : PathDecomposition C.toSimpleGraph), ∀ (i : Fin D.length), (D.bag i).card ≤ b)
: