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.

Estimated changes