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.

Read the Lean proof on GitHub

Description

Choose a minimum feedback edge set FF and one endpoint of each edge in FF. The set SS of chosen endpoints has cardinality at most ∣F∣|F|. Every edge of the induced graph G[V∖S]G[V\setminus S] remains in G−FG-F, so this induced graph is acyclic. Thus SS is a feedback vertex set and FVN⁡(G)≤∣S∣≤∣F∣=FEN⁡(G)\operatorname{FVN}(G)\leq |S|\leq |F|=\operatorname{FEN}(G).