### Abstract

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.

BSD License### Topics

### Theories of Linear_Inequalities

- Missing_Matrix
- Missing_VS_Connect
- Basis_Extension
- Sum_Vec_Set
- Integral_Bounded_Vectors
- Cone
- Convex_Hull
- Normal_Vector
- Dim_Span
- Fundamental_Theorem_Linear_Inequalities
- Farkas_Lemma
- Farkas_Minkowsky_Weyl
- Decomposition_Theorem
- Mixed_Integer_Solutions
- Integer_Hull