Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable_of_monotone

Modification history

2021-09-30 11:12
src/measure_theory/constructions/borel_space.lean
chore(order/basic): rename monotonicity concepts (#9383) …
Deleted measurable_of_monotoneView 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)
Modified measurable_of_monotoneView on Github →
2021-07-14 10:14
src/measure_theory/borel_space.lean
feat(measure_theory/borel_space): a monotone function is measurable (#8045)
Added measurable_of_monotoneView on Github →