Please explain in the docstring why do we need f to be continuous (I guess, otherwise one can put different functions along different parallel lines, some are differentiable, some aren't).
Also, is it measurable as a function of the pair (x, v) (even if "yes", IMHO this generalization shouldn't block the PR but should be mentioned in the docs)?
bors d+

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

It is indeed measurable as a function of (x, v), and this follows from the same argument applied to the function on (E x E) x k mapping (x, v, t) to f (x + tv). I have added this to the file. Unfortunately, to get somewhat optimal second countability assumptions for this, I had to improve a result in a previous file. This means that the PR is now bigger (it also proves that if a subset is separable then so is its linear span), and that the delegation no longer makes sense. So, I am putting it back to awaiting-review.

This PR/issue depends on:

• [Merged by Bors] - feat: the linear span of a separable set is separable #7115
• [Merged by Bors] - feat: better junk value for fderivWithin at isolated points #7117
  By Dependent Issues (🤖). Happy coding!

Build failed (retrying...):

• Build

Build failed (retrying...):

• Build

Build failed (retrying...):

• Build

bors r+

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style