Minimax theorem

Stream: Is there code for X?

[Rodolfo R. Soldati]

Do we have some implementation of the Minimax theorem?

I have seen some recent movement of people working on this to include in mathlib, but looking at the library did not lead anywhere. If someone has a more local implementation or prototype would also be sufficient.