-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(measure_theory/integral/set_integral): update old lemmas that were in comments at the end of the file #9111
Conversation
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
bors r+ |
…ere 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. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
Pull request successfully merged into master. Build succeeded: |
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
andset_integral_mono_set
are also moved to relevant sections.