Farkas lemma ($Az=b,z\ge 0\text{or}{A}^{T}y\ge 0,b^{T}y<0$)

Exactly one of the two displayed systems is feasible. Closedness of finitely generated cones and the Fenchel-Moreau theorem applied to a cone's indicator functional provide a proof through its polar cone. It yields a nonnegative multiplier certificate when a finite system of linear inequalities is inconsistent.

Such a vector certifies that $Cx\le d$ has no solution: the nonnegative weighted sum of the constraints would give $0\le d^{T}y<0$. Conversely, Farkas lemma supplies one whenever the system is inconsistent.