-
Notifications
You must be signed in to change notification settings - Fork 298
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] - feat(measure_theory/interval_integral): FTC-2 for the open set #5733
Conversation
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.
I'm in favour of this change. I left a few stylistic comments.
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.
LGTM, let's pass on to the measure theory people.
@robertylewis I think we were just waiting for their approval, I don't think there was a specific question. |
@robertylewis I haven't worked on the measure theory library, so didn't want to merge it on my own authority ... maybe it's ok if it looks good to you too. |
It looks unlikely to be controversial and very easy to fix if it is, and I get the sense the measure theory people are busy these days, so let's just merge! bors merge |
A follow-up to #4945. I replaced `integral_eq_sub_of_has_deriv_at'` with a stronger version that holds for functions that have a derivative on an `Ioo` (as opposed to an `Ico`). Inspired by [this](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/FTC-2.20on.20open.20set/near/222177308) conversation on Zulip. I also emended docstrings to reflect changes made in #5647.
Pull request successfully merged into master. Build succeeded: |
A follow-up to #4945. I replaced
integral_eq_sub_of_has_deriv_at'
with a stronger version that holds for functions that have a derivative on anIoo
(as opposed to anIco
). Inspired by this conversation on Zulip.I also emended docstrings to reflect changes made in #5647.