-
Notifications
You must be signed in to change notification settings - Fork 49
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
generalizations #1147
generalizations #1147
Conversation
The proofs are a bit longer but this is a strict generalizations, since the CI is green, I plan to merge soon @CohenCyril @zstone1 |
Looks good to me, and we should merge. That beeing said, the proofs might be shorter by doing a wlog that goes back to the previous statement. However, we may have more local lemmas asserting the existence of the limit, e.g. Lemma nonincreasing_at_right_is_cvg (f : R -> R) a :
(\forall x \near a^'+, {in `]a, x[, nonincreasing_fun f}) ->
(\forall x \near a^'+, has_ubound (f @` ]a, x[) ->
cvg (f x @[x --> a ^'+]). but it can wait for another PR |
Agreed I'm happy to merge anything that makes the code better. On a topological note, the "right-sided topology on R" AKA the "Sogenfrey line" captures a lot of this nicely. So you can talk about "locally in the Sogenfrey line". This has come up before, so maybe I'll write a PR to add it with the relevant lemmas for this application. |
c90bc25
to
e569271
Compare
* generalizations
* generalizations
Motivation for this change
This generalizes a few technical lemmas in
realfun.v
Things done/to do
CHANGELOG_UNRELEASED.md
Compatibility with MathComp 2.0
TODO: HB port
to make sure someone ports this PR tothe
hierarchy-builder
branch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.