Commit 2021-07-14 13:57 7d53431e

feat(measure_theory/integration): if a function has bounded integral on all sets of finite measure, then it is integrable (#8297) If the measure is sigma-finite and a function has integral bounded by some C for all measurable sets with finite measure, then its integral over the whole space is bounded by that same C. This can be used to show that a function is integrable.