Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ae_measurable_restrict_of_antimono_on

Modification history

2021-09-27 10:29
src/measure_theory/constructions/borel_space.lean
chore(order): globally replace "antimono" with "antitone" (#9400) …
Deleted ae_measurable_restrict_of_antimono_onView on Github →
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_antimono_onView on Github →