Add lemmas on divergent sequences

math-comp / analysis

Mathematical Components compliant Analysis Library

Other

200 stars 44 forks source link

Add lemmas on divergent sequences #1304

Closed Yosuke-Ito-345 closed 1 week ago

Yosuke-Ito-345 commented 1 month ago

Motivation for this change

fixes #1261

@affeldt-aist @hoheinzollern Add lemmas cvg_pinftyP and cvg_ninftyP in realfun.v. These are the infinite versions of lemmas cvg_at_leftP and cvg_at_rightP.

Checklist

[x] added corresponding entries in CHANGELOG_UNRELEASED.md
[ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

Read this Checklist
Put a milestone if possible
Check labels

Yosuke-Ito-345 commented 1 month ago

Sorry, there are bugs. I made a mistake again... I will fix them later.

Yosuke-Ito-345 commented 1 month ago

The bugs seem to be removed. Could you review the code?

Yosuke-Ito-345 commented 2 weeks ago

Could anyone review this PR?

affeldt-aist commented 2 weeks ago

it looks like this PR is adding .DS_Store files to classical, theories, and altreals, they should be removed