Commit 2020-11-18 21:10 abb0b678

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.