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 src/analysis/asymptotics.lean

Modified src/analysis/calculus/inverse.lean

added theorem approximates_linear_on.to_local_homeomorph_coe

deleted theorem approximates_linear_on.to_local_homeomorph_to_fun

added theorem has_strict_fderiv_at.to_local_homeomorph_coe

deleted theorem has_strict_fderiv_at.to_local_homeomorph_to_fun

Modified src/data/equiv/local_equiv.lean

added theorem equiv.to_local_equiv_coe

deleted theorem equiv.to_local_equiv_inv_fun

added theorem equiv.to_local_equiv_symm_coe

deleted theorem equiv.to_local_equiv_to_fun

modified theorem local_equiv.bij_on_source

added theorem local_equiv.coe_mk

added theorem local_equiv.coe_symm_mk

added theorem local_equiv.coe_trans

added theorem local_equiv.coe_trans_symm

modified theorem local_equiv.image_source_eq_target

modified theorem local_equiv.image_trans_source

added theorem local_equiv.inv_fun_as_coe

modified theorem local_equiv.inv_image_target_eq_source

modified theorem local_equiv.inv_image_trans_target

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_inv_fun

deleted theorem local_equiv.of_set_to_fun

added theorem local_equiv.prod_coe

added theorem local_equiv.prod_coe_symm

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

added theorem local_equiv.restr_coe_symm

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

modified theorem local_equiv.source_subset_preimage_target

deleted theorem local_equiv.symm_inv_fun

deleted theorem local_equiv.symm_to_fun

modified theorem local_equiv.target_subset_preimage_source

added theorem local_equiv.to_fun_as_coe

deleted theorem local_equiv.trans_apply

deleted theorem local_equiv.trans_inv_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

Modified src/geometry/manifold/basic_smooth_bundle.lean

deleted theorem basic_smooth_bundle_core.chart_at_inv_fun_fst

deleted theorem basic_smooth_bundle_core.chart_at_to_fun_fst

added theorem basic_smooth_bundle_core.coe_chart_at_fst

added theorem basic_smooth_bundle_core.coe_chart_at_symm_fst

added theorem tangent_bundle_model_space_coe_chart_at

added theorem tangent_bundle_model_space_coe_chart_at_symm

added def trivial_basic_smooth_bundle_core

Modified src/geometry/manifold/manifold.lean

added def continuous_pregroupoid

Modified src/geometry/manifold/mfderiv.lean

added theorem bundle_mfderiv_chart

deleted theorem bundle_mfderiv_chart_inv_fun

added theorem bundle_mfderiv_chart_symm

deleted theorem bundle_mfderiv_chart_to_fun

added theorem local_homeomorph.mdifferentiable.comp_symm_deriv

deleted theorem local_homeomorph.mdifferentiable.inv_fun_to_fun_deriv

deleted theorem local_homeomorph.mdifferentiable.mdifferentiable_at_inv_fun

added theorem local_homeomorph.mdifferentiable.mdifferentiable_at_symm

deleted theorem local_homeomorph.mdifferentiable.mdifferentiable_at_to_fun

added theorem local_homeomorph.mdifferentiable.symm_comp_deriv

deleted theorem local_homeomorph.mdifferentiable.to_fun_inv_fun_deriv

added theorem mdifferentiable_at_atlas

deleted theorem mdifferentiable_at_atlas_inv_fun

added theorem mdifferentiable_at_atlas_symm

deleted theorem mdifferentiable_at_atlas_to_fun

added theorem mdifferentiable_on_atlas

deleted theorem mdifferentiable_on_atlas_inv_fun

added theorem mdifferentiable_on_atlas_symm

deleted theorem mdifferentiable_on_atlas_to_fun

added theorem model_with_corners.mdifferentiable

added theorem model_with_corners.mdifferentiable_on_symm

deleted theorem model_with_corners_mdifferentiable_on_inv_fun

deleted theorem model_with_corners_mdifferentiable_on_to_fun

Modified src/geometry/manifold/real_instances.lean

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem ext_chart_at_coe

added theorem ext_chart_at_coe_symm

added theorem ext_chart_at_continuous_at

deleted theorem ext_chart_at_continuous_at_to_fun

added theorem ext_chart_at_continuous_on

deleted theorem ext_chart_at_continuous_on_inv_fun

added theorem ext_chart_at_continuous_on_symm

deleted theorem ext_chart_at_continuous_on_to_fun

deleted theorem ext_chart_continuous_at_inv_fun'

deleted theorem ext_chart_continuous_at_inv_fun

added theorem ext_chart_continuous_at_symm'

added theorem ext_chart_continuous_at_symm

modified theorem ext_chart_preimage_inter_eq

added theorem model_with_corners.continuous_symm

added theorem model_with_corners.left_inv'

added theorem model_with_corners.left_inv

added theorem model_with_corners.mk_coe

added theorem model_with_corners.mk_coe_symm

added theorem model_with_corners.right_inv

added theorem model_with_corners.target

added theorem model_with_corners.to_local_equiv_coe

added theorem model_with_corners.to_local_equiv_coe_symm

added theorem model_with_corners.unique_diff

added theorem model_with_corners.unique_diff_at_image

added theorem model_with_corners.unique_diff_preimage

added theorem model_with_corners.unique_diff_preimage_source

deleted theorem model_with_corners_inv_fun_comp

deleted theorem model_with_corners_left_inv

deleted theorem model_with_corners_right_inv

added theorem model_with_corners_self_coe

added theorem model_with_corners_self_coe_symm

modified theorem model_with_corners_self_local_equiv

deleted theorem model_with_corners_target

Modified src/topology/local_homeomorph.lean

added theorem homeomorph.to_local_homeomorph_coe

added theorem homeomorph.to_local_homeomorph_coe_symm

deleted theorem homeomorph.to_local_homeomorph_inv_fun

modified theorem homeomorph.to_local_homeomorph_source

modified theorem homeomorph.to_local_homeomorph_target

deleted theorem homeomorph.to_local_homeomorph_to_fun

modified theorem local_homeomorph.apply_eq_of_eq_on_source

added theorem local_homeomorph.coe_coe

added theorem local_homeomorph.coe_coe_symm

added theorem local_homeomorph.coe_trans

added theorem local_homeomorph.coe_trans_symm

deleted theorem local_homeomorph.continuous_at_inv_fun

added theorem local_homeomorph.continuous_at_symm

deleted theorem local_homeomorph.continuous_at_to_fun

added theorem local_homeomorph.continuous_on_symm

modified theorem local_homeomorph.image_open_of_open

modified theorem local_homeomorph.image_trans_source

modified theorem local_homeomorph.inv_apply_eq_of_eq_on_source

added theorem local_homeomorph.inv_fun_eq_coe

deleted theorem local_homeomorph.inv_fun_tendsto

modified theorem local_homeomorph.inv_image_trans_target

added theorem local_homeomorph.left_inv

added theorem local_homeomorph.map_source

added theorem local_homeomorph.map_target

added theorem local_homeomorph.mk_coe

added theorem local_homeomorph.mk_coe_symm

added theorem local_homeomorph.of_set_coe

deleted theorem local_homeomorph.of_set_inv_fun

modified theorem local_homeomorph.of_set_source

modified theorem local_homeomorph.of_set_symm

modified theorem local_homeomorph.of_set_target

deleted theorem local_homeomorph.of_set_to_fun

added theorem local_homeomorph.prod_coe

added theorem local_homeomorph.prod_coe_symm

deleted theorem local_homeomorph.prod_inv_fun

deleted theorem local_homeomorph.prod_to_fun

added theorem local_homeomorph.refl_coe

deleted theorem local_homeomorph.refl_inv_fun

modified theorem local_homeomorph.refl_source

modified theorem local_homeomorph.refl_symm

modified theorem local_homeomorph.refl_target

deleted theorem local_homeomorph.refl_to_fun

added theorem local_homeomorph.restr_coe

added theorem local_homeomorph.restr_coe_symm

deleted theorem local_homeomorph.restr_inv_fun

deleted theorem local_homeomorph.restr_to_fun

added theorem local_homeomorph.right_inv

deleted theorem local_homeomorph.symm_inv_fun

deleted theorem local_homeomorph.symm_to_fun

added theorem local_homeomorph.tendsto_symm

added theorem local_homeomorph.to_fun_eq_coe

added theorem local_homeomorph.to_homeomorph_coe

deleted theorem local_homeomorph.to_homeomorph_inv_fun

added theorem local_homeomorph.to_homeomorph_symm_coe

deleted theorem local_homeomorph.to_homeomorph_to_fun

deleted theorem local_homeomorph.trans_inv_fun

modified theorem local_homeomorph.trans_source''

modified theorem local_homeomorph.trans_source'

modified theorem local_homeomorph.trans_source

modified theorem local_homeomorph.trans_target''

modified theorem local_homeomorph.trans_target'

modified theorem local_homeomorph.trans_target

deleted theorem local_homeomorph.trans_to_fun

Modified src/topology/topological_fiber_bundle.lean

added theorem bundle_trivialization.coe_coe

added theorem bundle_trivialization.coe_fst

added theorem bundle_trivialization.coe_mk