mathlib documentation


We define a proper cone as a nonempty, closed, convex cone. Proper cones are used in defining conic programs which generalize linear programs. A linear program is a conic program for the positive cone. We then prove Farkas' lemma for conic programs following the proof in the reference below. Farkas' lemma is equivalent to strong duality. So, once have the definitions of conic programs and linear programs, the results from this file can be used to prove duality theorems.


In the next few PRs (already sorry-free), we will add the definition and prove several properties of proper cones and finally prove the cone version of Farkas' lemma (2.3.4 in the reference).

The next steps are:

References #


The closure of a convex cone inside a real inner product space is a convex cone. This construction is mainly used for defining maps between proper cones.