Proof of `Feedback vertex number is at most feedback edge number`
groundedproofs/Lax379983Proofs/FeedbackNumberComparison.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 edge set and one endpoint of each edge in . The set of chosen endpoints has cardinality at most . Every edge of the induced graph remains in , so this induced graph is acyclic. Thus is a feedback vertex set and .