Theorem measurable_iInf_of_upperSemicontinuous

Modification history

2026-10-30 20:28
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
refactor(MeasureTheory/Constructions/BorelSpace/Order): regroup sections and weaken hypotheses (#45475) …
Modified measurable_iInf_of_upperSemicontinuousView on Github →
2026-04-19 20:26
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
feat(MeasureTheory/BorelSpace): add `measurable_iSup_of_lowerSemicontinuous` (#37552) …
Added measurable_iInf_of_upperSemicontinuousView on Github →