mathlib

1dafd0f7 - feat(measure_theory/integrable_on): a monotone function is integrable on any compact subset (#8336)