subtypes and continuous functions

[zstone1]

Two related things. Now that pointed is gone from topology, we can canonically add topology/uniform/pseudometric on set_val. This now just a few easy instances.

Then we define a mixin for continuous functions. We build two structures from this. One is just Continuous for use with subtypes, and ContinuousFun for mixing with the Fun hierarchy using subspaces. And a bunch of lemmas for converting between them. Then we endow the set of continuous functions with various topologies in the ArrowAsT modules in function_spaces.v. In general I'd like to say "if arrow has a topology, then continuousType` inherits it, but I don't know how to say that in general, so it's fine to just manually do the instances in those modules.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[mkerjean]

I cruelly lack the expertise in HB to review this pull request. I hope @affeldt-aist will be able to add insight. From the mathematical perspective, this all seems great and potentially very useful.

[affeldt-aist]

I fixed the changelog, maybe you are using the automatic tool to generate it but it looks like it does not handle HB definitions very well. I added very scarce documentation for the new definitions (and also spotted a few one that were not yet documented), you may want to fix/complete what I wrote. And then the usual linting.