Proof of `Treedepth and Δ-forestwidth` (2nd statement)
groundedproofs/Lax461425Proofs/TreedepthForestwidth.lean · lax-461425
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
Each vertex is placed at its unique top node. Vertices at a node of depth receive the ranks in a fixed order, and is an ancestor of if it has smaller rank and its top node is an ancestor of that of . The endpoints of an edge lie in a common bag, so their top nodes are both ancestors of that node, hence comparable.