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

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[VS]G[V\setminus S] remains in GFG-F, so this induced graph is acyclic. Thus SS is a feedback vertex set and FVN(G)SF=FEN(G)\operatorname{FVN}(G)\leq |S|\leq |F|=\operatorname{FEN}(G).