mathlib3

d989ff47 - feat(measure_theory/lebesgue_measure): integral as volume between graphs (#5932)

feat(measure_theory/lebesgue_measure): integral as volume between graphs (#5932) I show that the integral can compute the volume between two real-valued functions. I start with the definition `region_between`, I prove that the region between two functions is a `measurable_set`, and then I prove two integral theorems. Help from @hrmacbeth and @benjamindavidson. Co-authored-by: Andrew Souther <65313859+asouther4@users.noreply.github.com> Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>