Commit 2021-09-14 06:36 5aaa5faa

chore(measure_theory/integral/set_integral): update old lemmas that were in comments at the end of the file (#9111) The file set_integral had a list of lemmas in comments at the end of the file, which were written for an old implementation of the set integral. This PR deletes the comments, and adds the corresponding results when they don't already exist. The lemmas set_integral_congr_set_ae and set_integral_mono_set are also moved to relevant sections.