Commit 2022-01-20 16:01 b5e542d3

View on Github →

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.

Estimated changes

Modified src/measure_theory/group/basic.lean

Modified src/measure_theory/measurable_space.lean

added theorem exists_measurable_piecewise_nat

added theorem measurable.find

added def measurable_equiv.pi_measurable_equiv_tprod

modified theorem measurable_find

modified theorem measurable_find_greatest'

modified theorem measurable_find_greatest

modified theorem measurable_from_prod_encodable

modified theorem measurable_set_pi_of_nonempty

modified theorem measurable_tprod_elim'

modified theorem measurable_tprod_elim

modified theorem measurable_update

Modified src/measure_theory/measure/haar.lean