Proof of `Treewidth is at most feedback vertex number plus one`
groundedproofs/Lax379983Proofs/TreewidthBound.lean · lax-379983
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Choose a minimum feedback vertex set . The remaining forest has a tree decomposition with at most two vertices in each bag: for a nonempty forest, extend it to a tree, root it, and use each vertex together with its parent as a bag, with a singleton bag at the root. For the empty forest, use one empty bag. Adding to every bag covers all original edges and preserves connectedness of the bags containing each vertex. Each new bag has at most vertices, so its width is at most .