A feasible linear program in standard form bounded below attains its minimum

Attainment for a linear program in standard form. Let $W \in \mathbb{R}^{m\times n}$, $q \in \mathbb{R}^n$ and $d \in \mathbb{R}^m$, and consider

If the feasible set is nonempty and the objective is bounded below on it, then the infimum is attained: some feasible $y_0$ satisfies $q^{\mathsf T} y_0 \le q^{\mathsf T} y$ for every feasible $y$.

Unlike a continuous function on a compact set, a linear function on an unbounded polyhedron has no a priori reason to attain its infimum; that it does is a genuinely polyhedral phenomenon, and it is what allows optimal bases, complementary slackness and the simplex method to be discussed at all. The proof here goes through the closedness of the finitely generated cone spanned by the augmented columns $(q_j, W_{\cdot j}) \in \mathbb{R}^{1+m}$.

Formalization note. Boundedness below is stated as the existence of a single $\beta$ below all feasible objective values, and optimality of $y_0$ as a pointwise inequality against all feasible $y$; no separate notion of "optimal value" is introduced.