Proof of `The exact hull is nonempty precisely at feasible targets`
groundedproofs/Lax263307Proofs/HullNonempty.lean · lax-263307
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
The exact hull is nonempty if and only if there is an independent set of the target cardinality.
Proof strategy
A convex hull is nonempty precisely when its generating set is nonempty. Unfolding the generating set gives the claimed independent set.
Attribution
Bonnet–Chang, Section 5.1, equation (20).