Commit 2024-06-11 07:52 15309603
View on Github →feat(MeasureTheory/Integral/Lebesgue): setLintegral_pos_iff (#13172)
(MeasureTheory/Integral/Lebesgue): setLintegral_pos_iff
For a given Measurable set sand a AEMeasurable function f, the subset of s where f is nonnegative is of nonnegative measure iff the lintegral of fon s is nonnegative.