Weyl: the cone generated by finitely many vectors of ℝ^m is closed

Weyl's theorem on finitely generated cones. Let $v_1,\dots,v_n \in \mathbb{R}^m$. The cone they generate,

is a closed subset of $\mathbb{R}^m$.

Closedness is not automatic: the cone is the image of the closed but unbounded set $\mathbb{R}^n_{\ge 0}$ under a linear map, and linear images of closed sets need not be closed. The result is one half of the Minkowski-Weyl theorem (a V-cone is an H-cone), and it is the topological input to Farkas' lemma, to linear programming duality, and to the fact that the feasible set of a stochastic program with fixed recourse is closed.

Formalization note. Vectors are functions out of Fin m, carrying the product topology, which for a finite index set is the usual Euclidean topology. The generators are given as a family v : Fin n → (Fin m → ℝ); taking v j to be the $j$-th column of a matrix $A$ gives the closedness of $\{A y : y \ge 0\}$.