mathlib3

b5e542d3 - feat(measure_theory/measurable_space): defining a measurable function on countably many pieces (#11532)

feat(measure_theory/measurable_space): defining a measurable function on countably many pieces (#11532) Also, remove `open_locale classical` in this file and add decidability assumptions where needed. And add a few isolated useful lemmas.