Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(measure_theory/measure/set_integral): new lemma integral_Union #9093

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(measure_theory/measure/set_integral): new lemma integral_Union #9093

wants to merge 3 commits into from

Conversation

sgouezel
Copy link
Collaborator

@sgouezel sgouezel commented Sep 8, 2021

Requested for #9008

@sgouezel sgouezel mentioned this pull request Sep 8, 2021
Closed
2 tasks
@JasonKYi
Copy link
Member

JasonKYi commented Sep 8, 2021

Thanks a lot for this PR!

@sgouezel sgouezel added the awaiting-review The author would like community review of the PR label Sep 8, 2021
RemyDegenne
RemyDegenne approved these changes Sep 9, 2021
View reviewed changes
Copy link
Collaborator

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It all looks good. I have only a few minor comments about spaces and replacing apply by exact.

src/measure_theory/integral/set_integral.lean Outdated Show resolved Hide resolved
src/measure_theory/integral/set_integral.lean Outdated Show resolved Hide resolved
src/measure_theory/integral/set_integral.lean Outdated Show resolved Hide resolved
src/measure_theory/integral/set_integral.lean Outdated Show resolved Hide resolved
@RemyDegenne
Copy link
Collaborator

Just so you know: I am currently making a PR in which I deal with the other commented out old lemmas at the bottom of set_integral (adding them to the file if they are missing, deleting them if they already exists). I just want to make sure that you are not doing the same thing.

@sgouezel @RemyDegenne
Apply suggestions from code review
f63e4d0 
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
@sgouezel
Copy link
Collaborator Author

sgouezel commented Sep 9, 2021

Thanks for the review, and thanks for telling me about the other lemmas. I'm not working on them, I only did this one because it was needed by @JasonKYi

@RemyDegenne RemyDegenne mentioned this pull request Sep 9, 2021
Closed
1 task
@JasonKYi JasonKYi mentioned this pull request Sep 10, 2021
Closed
6 tasks
@urkud
Copy link
Member

urkud commented Sep 11, 2021

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 11, 2021
bors bot pushed a commit that referenced this pull request Sep 11, 2021
@sgouezel
feat(measure_theory/measure/set_integral): new lemma integral_Union (#…
4c96b8a 
…9093)
@bors
Copy link

bors bot commented Sep 11, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/measure/set_integral): new lemma integral_Union [Merged by Bors] - feat(measure_theory/measure/set_integral): new lemma integral_Union Sep 11, 2021
@bors bors bot closed this Sep 11, 2021
@bors bors bot deleted the integral_Union branch September 11, 2021 04:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@RemyDegenne RemyDegenne RemyDegenne approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@sgouezel @JasonKYi @RemyDegenne @urkud