-
Notifications
You must be signed in to change notification settings - Fork 45
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
Add lemmas on divergent sequences #1304
Add lemmas on divergent sequences #1304
Conversation
Sorry, there are bugs. |
The bugs seem to be removed. |
Could anyone review this PR? |
it looks like this PR is adding |
a8479f6
to
9b40b0a
Compare
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.
@hoheinzollern , ok to merge if the CI turns green?
4b1522d
to
648ca44
Compare
Motivation for this change
fixes #1261
@affeldt-aist @hoheinzollern
Add lemmas
cvg_pinftyP
andcvg_ninftyP
inrealfun.v
.These are the infinite versions of lemmas
cvg_at_leftP
andcvg_at_rightP
.Checklist
CHANGELOG_UNRELEASED.md
Reference: How to document
Reminder to reviewers