Duality theory in linear optimization and its extensions -- formally verified

Martin Dvorak, Vladimir Kolmogorov

Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state…