Padding path decompositions by a boundary #
Insert a fixed boundary in every bag and at both ends. The added boundary may overlap the induced copy of the original graph.
theorem
Algebraic.Cutwidth.PathDecomposition.exists_pad
{V W : Type}
{G : SimpleGraph V}
{H : SimpleGraph W}
(D : PathDecomposition G)
(f : G ↪g H)
(X : Finset W)
(cover : ∀ (w : W), w ∈ Set.range ⇑f ∨ w ∈ X)
{b : ℕ}
(bound : ∀ (i : Fin D.length), (D.bag i).card ≤ b)
:
Extend an induced copy's decomposition by adding X to all bags and as
both endpoints. Every vertex outside the copy must lie in X.