affeldt-aist

https://github.com/math-comp/math-comp/blob/36dbdd6bb3c5e2a46c075ab0344920466eaf4fea/mathcomp/algebra/ssrnum.v#L427 `archiDomain` -> `archiRealDomain` similarly: `archiField` -> `archiRealField` see conversation item https://github.com/math-comp/math-comp/pull/1235#issuecomment-2199976942

##### Motivation for this change ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document) ##### Reminder to...

##### Motivation for this change the proof is obtained by exploiting the symmetry between `at_left` and `at_right` proof used in work in progress by @IshiguroYoshihiro ##### Checklist - [x] added...

fixes #330 (floor and ceil subsumed by MathComp)

2

##### Motivation for this change fixes #330 ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document) ##### Reminder...

generalize lime_sup_ge0

1

##### Motivation for this change the easy bit of issue #1135 ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ Reference:...

Co-authored-by: @JeremyDubut Co-authored-by: @AkihisaYamada ##### Motivation for this change ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ Reference: [How to...

fixes #1248 (`to_set` / `xsection`)

1

##### Motivation for this change TODO: maybe also rename `xsection` to `xsect`, that's clear enough. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding...

https://github.com/math-comp/analysis/blob/53a6bff77bd285d33cb91094cfbee9e092837f34/theories/topology.v#L4000 the `to_set` notation is declared here and also in other files but is redundant with the `xsection` definition (modulo the Prop/bool difference)

##### Motivation for this change See issue #965 Provides also the Borel-Cantelli lemma (and the limit superior of the sequence of sets) and continuity of the indefinite integral at the...

##### Motivation for this change This is a first step towards fixing the issue https://github.com/math-comp/analysis/issues/1225 : rename `setD_closed` to `setSD_closed` so that `setDI_closed` can be renamed `setD_closed` later. ##### Checklist...