Shift the matrix by adding a positive constant to every entry, so all entries are positive. Apply finite-dimensional linear-programming duality (Strong Duality For Linear Programming) to the dual programs $$ XA \ge \mathbf{1}, \quad X \ge 0 $$ and $$ AY \le \mathbf{1}, \quad Y \ge 0. $$ The dual optimal solutions have a common objective value $w>0$. Normalizing the vectors by $w$ gives mixed strategies $x^*$ and $y^*$, and the inequalities become the minimax optimality inequalities with value $1/w$ via the simplex bound transfer Pointwise Bounds Are Simplex Bounds. Weak duality Maximin is Bounded by Minimax closes the sandwich, and undoing the constant shift gives the original game.

This proof route is recorded as a candidate rather than selected: the library's chosen formalisation route for Von Neumann Minimax Theorem is the simplified-Loomis induction (Minimax via the All-Ones Specialization of Loomis). The LP-duality route is now viable in EconCSLib via the strong-duality node (Farkas → LP strong duality) landed in #71, but has not been carried through to a Lean proof.

References

• [MFoGT, Thm. 2.3.2 and proof after Thm. 2.3.2] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. LP duality proof of von Neumann minimax.