affeldt-aist

@Tragicus We've merged PR #85 which should contained all the commits of this PR, so that it should be ok to close.

> Your second proofreading does not appear in the list of commits. Really? I thought I squashed my last commits into one. > Besides, the definition of linear_affine was broken...

This commit https://github.com/math-comp/analysis/pull/752/commits/b4230f9a0d02c068f3c457c0eed74ac6dd988c9b might be a solution for the case `{within A, continuous f}`. Can you confirm? (I used the lemma `itv_continuous_inj_le` in realfun.v for testing but a quick look...

> ``` > Lemma subspaceT_continuous {U} A (B : set U) (f : {fun A >-> B}) : > {within A, continuous f} -> continuous (f : subspace A ->...

NB: `\o` has been moved (as `\;`) to `classical_sets.v` as well as a couple of lemmas

> @affeldt-aist this seems reasonably ready for nearly three months now, would you assign and merge? I would have said okay a few days ago but the generalization requested in...

I didn't try but according to https://hal.science/hal-04225130/document (see page 2) and since we are not building any deep hierarchy using canonicals in infotheo (indeed we are now using HB for...

I am not saying that we should do it asap though, on the contrary, considering practical aspects, it is maybe more reasonable to clean up infotheo for robustmean as much...

NB: wip by @yoshihiro503

See https://github.com/math-comp/math-comp/pull/937