Commit 2026-04-07 16:25 ff84feb2

View on Github →

feat(Topology/Sion): the minimax theorem of von Neumann - Sion (#31560) Prove Sion.exists_isSaddlePointOn : Let X and Y be convex subsets of topological vector spaces E and F, X being moreover compact, and let f : X × Y → ℝ be a function such that

for all x, f(x, ⬝) is upper semicontinuous and quasiconcave
for all y, f(⬝, y) is lower semicontinuous and quasiconvex Then inf_x sup_y f(x,y) = sup_y inf_x f(x,y). The classical case of the theorem assumes that f is continuous, f(x, ⬝) is concave, f(⬝, y) is convex. As a particular case, one get the von Neumann theorem where f is bilinear and E, F are finite dimensional. We follow the proof of Komiya (1988).

Remark on implementation

The essential part of the proof holds for a function f : X → Y → β, where β is a complete dense linear order.
We have written part of it for just a dense linear order,
On the other hand, if the theorem holds for such β, it must hold for any linear order, for the reason that any linear order embeds into a complete dense linear order. Although the Dedekind McNeille completion (docs#DedekindCut) furnishes a complete lattice, it is not dense in general, so that this result does not seem to be known to Mathlib yet.
When β is ℝ, one can use Real.toEReal and one gets a proof for ℝ.