Commit 2024-10-12 07:45 47521133
View on Github →chore(MeasureTheory/Integral/SetIntegral): fix lemma names (#17658) Rename:
integral_empty
->setIntegral_empty
integral_union
->setIntegral_union
integral_univ
->setIntegral_univ
setIntegral_congr
->setIntegral_congr_fun
setIntegral_congr₀
->setIntegral_congr_fun₀
setLIntegral_congr_set_ae
->setIntegral_congr_set
From PFR