I was formalizing some linear programming in Lean and came across one of the most surprisingly difficult to prove theorems. ::: {#thm-closed-convex-cones} Let $A : \mathbb{R}^m \to \mathbb{R}^n$ be a linear transformation. Then the set $$ { A x : : : x \ge 0 } $$ is closed in . . . Read more