Commit 2020-11-18 21:10 abb0b678
View on Github →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.