mathlib3

08a4542b - feat(measure_theory/function): Functions locally integrable on a set (#18673)

feat(measure_theory/function): Functions locally integrable on a set (#18673) This PR adds a definition for local integrability of a function on a set (a relative version of the existing "locally integrable"), and proves some elementary properties of this definition (in particular, functions continuous on `s` are locally integrable on `s`).