Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

modified theorem local_equiv.bij_on_source
added theorem local_equiv.coe_mk
added theorem local_equiv.coe_trans
added theorem local_equiv.left_inv
added theorem local_equiv.map_source
added theorem local_equiv.map_target
added theorem local_equiv.of_set_coe
deleted theorem local_equiv.of_set_to_fun
added theorem local_equiv.prod_coe
deleted theorem local_equiv.prod_inv_fun
deleted theorem local_equiv.prod_to_fun
added theorem local_equiv.refl_coe
deleted theorem local_equiv.refl_inv_fun
deleted theorem local_equiv.refl_to_fun
added theorem local_equiv.restr_coe
deleted theorem local_equiv.restr_inv_fun
modified theorem local_equiv.restr_target
deleted theorem local_equiv.restr_to_fun
added theorem local_equiv.right_inv
deleted theorem local_equiv.symm_inv_fun
deleted theorem local_equiv.symm_to_fun
deleted theorem local_equiv.trans_apply
deleted theorem local_equiv.trans_inv_fun
modified theorem local_equiv.trans_source''
modified theorem local_equiv.trans_source'
modified theorem local_equiv.trans_source
modified theorem local_equiv.trans_target''
modified theorem local_equiv.trans_target'
modified theorem local_equiv.trans_target
deleted theorem local_equiv.trans_to_fun
added theorem ext_chart_at_coe
added theorem ext_chart_at_coe_symm
modified theorem ext_chart_preimage_inter_eq
deleted theorem model_with_corners_target
modified theorem local_homeomorph.refl_symm