feat(measure_theory): additions (#4324)
Many additional lemmas.
Notable addition: sequential limits of measurable functions into a metric space are measurable.
Rename `integral_map_measure` -> `integral_map` (to be consistent with the version for `lintegral`)
Fix the precedence of all notations for integrals. From now on `∫ x, abs ∥f x∥ ∂μ` will be parsed
correctly (previously it gave a parse error).
Some cleanup (moving lemmas, and some nicer presentation by opening locales and namespaces).
