Theorem lowerSemicontinuousOn_of_forall_isMaxOn_and_mem

Modification history

2026-04-07 16:25
Mathlib/Topology/Semicontinuity/Basic.lean
feat(Topology/Sion): the minimax theorem of von Neumann - Sion (#31560) …
Added lowerSemicontinuousOn_of_forall_isMaxOn_and_memView on Github →