affeldt-aist

https://github.com/math-comp/analysis/blob/91476c4c4e4b13bdfbfaa078e1033136f538c6c8/theories/charge.v#L414-L463 wanted: a generic approach to handle similar goals in R and \bar R

Missing notations in `itv.v`?

2

https://github.com/math-comp/analysis/blob/5d4db09b412ac521d67830bd1ba507aed567056c/theories/itv.v#L35-L40 I can find `[itv of ...]` but not `[lb of ...]`, etc.

https://github.com/math-comp/analysis/blob/f1290113c953bf3df6650bb774ce08556f1c8487/theories/convex.v#L144-L164 This implements "continuity up the endpoints", approach 1. Other approaches could have been (I am here reproducing contents from the conversion of now merged PR https://github.com/math-comp/analysis/pull/873): 2. We could...

\near F, P F

2

https://github.com/math-comp/analysis/blob/ceb11bd28d7a43f63238cd0f9039953059f097a3/theories/topology.v#L133 ~~should be `\forall y \near x, P y`~~ taken care of by PR #782

It might be nice for the users to be informed when using `HB.howto` (for example, by a message in the output) that they can increase the "depth search" to potentially...

`expR` shouldn't be defined in `sequences.v` (maybe)...

in particular, it lacks of examples

https://github.com/math-comp/analysis/blob/00fed879bee5f11108bc4ae998396f7bd249f01d/theories/measure.v#L2542-L2543

This branch/PR is to record the tentative port of `set.v` to MathComp 2. At the time of this writing, it is based on PR #84 (the port of finmap to...

Update description

1

The github "Description" for `finmap` says "Finite sets, finite maps, multisets and order". It should maybe be "Finite sets, finite maps, and multisets" now that `order` is in MathComp.