Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ae_measurable_restrict_of_monotone_on

Modification history

2021-07-20 08:59
src/measure_theory/borel_space.lean
feat(measure_theory/borel_space): generalize `monotone.measurable` to monotone on set (#8365)
Added ae_measurable_restrict_of_monotone_onView on Github →