Linear Inequalities

Ralph Bottesch, Alban Reynaud, René Thiemann

Archive of Formal Proofs 2019.


We formalize results about linear inqualities, mainly from Schrijver’s book. The main results are the proof of the fundamental theorem on linear inequalities, Farkas’ lemma, Carathéodory’s theorem, the Farkas-Minkowsky-Weyl theorem, the decomposition theorem of polyhedra, and Meyer’s result that the integer hull of a polyhedron is a polyhedron itself. Several theorems include bounds on the appearing numbers, and in particular we provide an a-priori bound on mixed-integer solutions of linear inequalities.


   AFP entry


author = {Ralph Bottesch and Alban Reynaud and René Thiemann},
title = {Linear Inequalities},
journal = {Archive of Formal Proofs},
month = jun,
year = 2019,
note = {\url{}, Formal proof development},
ISSN = {2150-914x},
Nach oben scrollen