Commit 2022-09-18 07:54 1dc531a0
View on Github →feat(measure_theory/integral): finiteness of lower Lebesgue integral (#16514) This PR proves that if a function is integrable and non-negative, then it's lower Lebesgue integral is finite.
feat(measure_theory/integral): finiteness of lower Lebesgue integral (#16514) This PR proves that if a function is integrable and non-negative, then it's lower Lebesgue integral is finite.