Proof of `Fourier–Motzkin elimination`
groundedproofs/Lax109476Proofs/Farkas.lean · lax-109476
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
Partition the rows according to the sign of the eliminated variable's coefficient. Combine every positive row with every negative row using nonnegative multipliers, and retain the zero rows. A finite family of compatible lower and upper bounds admits a witness for the removed variable.
Attribution
Adapted from Jyotirmoy Bhattacharya's MIT-licensed , revision 30c319dd52ca89cfa82a68352b1f39f4f3026fc2. The adapted files retain the copyright and license notices.