mathlib

f0c15be6 - feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions (#12985)

feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions (#12985) A function is almost everywhere strongly measurable if it is almost everywhere the pointwise limit of a sequence of simple functions. These are the functions that can be integrated in the most general version of the Bochner integral. As a prerequisite for the refactor of the Bochner integral, we define almost strongly measurable functions and build a comprehensive API for them, gathering in the file `strongly_measurable.lean` all facts that will be needed for the refactor. The API does not claim to be complete, but it is already pretty big.