Commit 2021-06-24 15:14 4801fa66

feat(measure_theory): the Vitali-Caratheodory theorem (#7766) This PR proves the Vitali-Carathéodory theorem, asserting that a measurable function can be closely approximated from above by a lower semicontinuous function, and from below by an upper semicontinuous function. This is the main ingredient in the proof of the general version of the fundamental theorem of calculus (when f' is just integrable, but not continuous).