Commit 2024-05-28 12:13 e0685aa8
View on Github →feat: add mul_iff right and mul_iff_left for (AE)(Strongly)Measurable (#12711)
Add the lemma that says that if f
is measurable, then f+g
is measurable iff g
is measurable. Then add the same but with g+f
, and the same lemmas about AEMeasurable, StronglyMeasurable and AEStronglyMeasurable.