affeldt-aist

memo: mentioned in PR #294

partially handed by PR #435?

Not a deep comment but you may want to consider the if/is/then/else syntax to write functions, e.g.: ```coq Fixpoint false_extend (s : seq bool) : cantor_space := if s is...

Update: Note that PR #267 has been closed and split into PR #283 (now merged) and PR #183 (to be merged shortly)

I am right to think that this issue has not yet been addressed?

Just for information. Compilation fails on my side at `FilteredEntourage_IsUniform` [1] while it looks like it should be going a bit further. It is actually the second time that I...

I haven't figured out weak_topologicalTypeMixin but maybe at least nbhs_of_open that will be used ought better be outisde of a builders section to stay accessible.

What it is the status of this PR?

So I guess we should update the PR. Since things have changed in two years, I wonder whether it would not be better to do a new PR.

I would be tempted to write: ``` Definition contraction (q : {nonneg R}) (f : {fun U >-> V}) := ((q%:num < 1) * q%:num.-lipschitz_U f)%type. ``` so that at...