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 s
and a AEMeasurable function f
, the subset of s
where f
is nonnegative is of nonnegative measure iff the lintegral of f
on s
is nonnegative.