Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Treewidth and Δ-forestwidth` (1st statement)

groundedproofs/Lax461425Proofs/TreewidthForestwidth.lean · lax-461425

What this proof establishes

no assumptions

thm✓Lax461425.TreewidthForestwidth (1st statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Root the tree at any node rr, take as parent the next node on the unique path to rr, and add a new root with an empty bag above rr. A vertex has a unique top node because every node containing it lies below each of its top nodes.