Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable_of_antimono

Modification history

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