mathlib4 feat(MeasureTheory): two lemmas on almost everywhere equality and positive lintegral

feat(MeasureTheory): two lemmas on almost everywhere equality and positive lintegral

Open gaetanserre opened this issue 1 year ago • 2 comments

Multiple results on almost everywhere equality and positive lintegral.

(MeasureTheory/Measure/MeasureSpaceDef): fun_ae_imp_set_ae Two functions are almost everywhere equal on their entire domain iff they are a.e equal on every subsets of their domain.
(MeasureTheory/Integral/Lebesgue): lintegral_positive If a function is nonnegative on a set of nonnegative measure, then its integral on this set is nonnegative.