Commit 2021-02-07 23:41 d989ff47

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.