Adding a boundary to all bags #
An induced copy of a graph has a path decomposition. Add a fixed vertex set to every bag and as both endpoint bags. If the fixed set covers the vertices outside the copy, the enlarged bags decompose the whole graph.
theorem
Algebraic.Cutwidth.PathDecomposition.Internal.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)
: