refactor(*): make continuous a structure (#5035)
Turn `continuous` into a structure, to make sure it is not unfolded too much by Lean.
After the change, inferring some types is harder to Lean (as it can not unfold further to find more information), so some help is needed at places. Especially, for `hf : continuous f` and `hg : continuous g`, I had to replace `hf.prod_mk hg` with `(hf.prod_mk hg : _)` a lot of times.
For `hf : continuous f` and `hs : is_open s`, the fact that `f^(-1) s` is open used to be `hf s hs`. Now, it is `hs.preimage hf`, just like it is for closed sets.
