Commit 2020-05-06 19:39 460d9d43
View on Github →refactor(data/equiv/local_equiv, topology/local_homeomorph): use coercions (#2603)
Local equivs and local homeomorphisms use e.to_fun x
and e.inv_fun x
, instead of coercions as in most of mathlib, as there were problems with coercions that made them unusable in manifolds. These problems have been fixed in Lean 3.10, so we switch to coercions for them also.
This is 95% a refactor PR, erasing .to_fun
and replacing .inv_fun
with .symm
in several files, and fixing proofs. Plus a few simp lemmas on the coercions to let things go smoothly. I have also linted all the files I have touched.