Mathlib Changelog
v4
Changelog
About
Github
Theorem
upperSemicontinuousOn_of_forall_isMinOn_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
upperSemicontinuousOn_of_forall_isMinOn_and_mem
View on Github →