Commit 2026-01-26 08:43 ba35fe04

View on Github →

feat(MeasureTheory/Probability): Generalize some theorems by replacing OrderClosedTopology with ClosedIciTopology (#34432) Theorems like MeasureTheory.L1.setToL1_nonneg only require ClosedIciTopology. This is part of my effort in solving https://github.com/RemyDegenne/brownian-motion/issues/350. I want to generalize the definition of leastGE to functions taking values in a space with ClosedIciTopology.

Estimated changes

modified theorem Measurable.lt
modified theorem measurableSet_Icc
modified theorem measurableSet_Ici
modified theorem measurableSet_Ico
modified theorem measurableSet_Iic
modified theorem measurableSet_Iio
modified theorem measurableSet_Ioc
modified theorem measurableSet_Ioi
modified theorem measurableSet_Ioo
modified theorem measurableSet_lt'
modified theorem measurableSet_lt
modified theorem measurableSet_uIcc
modified theorem measurableSet_uIoc
modified theorem measurable_lt
modified theorem nullMeasurableSet_Icc
modified theorem nullMeasurableSet_Ici
modified theorem nullMeasurableSet_Ico
modified theorem nullMeasurableSet_Iic
modified theorem nullMeasurableSet_Iio
modified theorem nullMeasurableSet_Ioc
modified theorem nullMeasurableSet_Ioi
modified theorem nullMeasurableSet_Ioo
modified theorem nullMeasurableSet_le
modified theorem nullMeasurableSet_lt'
modified theorem nullMeasurableSet_lt
modified theorem MeasureTheory.setToFun_mono