Commit 2023-01-06 13:58 956714e4

View on Github →

feat port: Logic.Equiv.LocalEquiv (#1052) aba57d4d3dae35460225919dcd82fe91355162f9

Estimated changes

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Logic/Equiv/LocalEquiv.lean

added theorem Equiv.refl_toLocalEquiv

added theorem Equiv.symm_toLocalEquiv

added def Equiv.toLocalEquiv

added def Equiv.transLocalEquiv

added theorem Equiv.trans_localEquiv_eq_trans

added theorem Equiv.trans_toLocalEquiv

added theorem LocalEquiv.EqOnSource.eqOn

added theorem LocalEquiv.EqOnSource.restr

added theorem LocalEquiv.EqOnSource.source_eq

added theorem LocalEquiv.EqOnSource.source_inter_preimage_eq

added theorem LocalEquiv.EqOnSource.symm'

added theorem LocalEquiv.EqOnSource.symm_eqOn

added theorem LocalEquiv.EqOnSource.target_eq

added theorem LocalEquiv.EqOnSource.trans'

added def LocalEquiv.EqOnSource

added theorem LocalEquiv.IsImage.apply_mem_iff

added theorem LocalEquiv.IsImage.iff_preimage_eq

added theorem LocalEquiv.IsImage.iff_symm_preimage_eq

added theorem LocalEquiv.IsImage.image_eq

added theorem LocalEquiv.IsImage.inter_eq_of_inter_eq_of_eq_on

added theorem LocalEquiv.IsImage.leftInvOn_piecewise

added theorem LocalEquiv.IsImage.of_image_eq

added theorem LocalEquiv.IsImage.of_symm_image_eq

added def LocalEquiv.IsImage.restr

added theorem LocalEquiv.IsImage.symm_apply_mem_iff

added theorem LocalEquiv.IsImage.symm_eq_on_of_inter_eq_of_eq_on

added theorem LocalEquiv.IsImage.symm_iff

added theorem LocalEquiv.IsImage.symm_image_eq

added theorem LocalEquiv.IsImage.symm_mapsTo

added def LocalEquiv.IsImage

added def LocalEquiv.Simps.symmApply

added theorem LocalEquiv.coe_symm_mk

added theorem LocalEquiv.coe_trans

added theorem LocalEquiv.coe_trans_symm

added def LocalEquiv.copy

added theorem LocalEquiv.copy_eq

added def LocalEquiv.disjointUnion

added theorem LocalEquiv.disjoint_union_eq_piecewise

added theorem LocalEquiv.eqOnSource_refl

added theorem LocalEquiv.eq_of_eq_on_source_univ

added theorem LocalEquiv.eq_symm_apply

added theorem LocalEquiv.exists_mem_target

added theorem LocalEquiv.forall_mem_target

added theorem LocalEquiv.image_eq_target_inter_inv_preimage

added theorem LocalEquiv.image_source_eq_target

added theorem LocalEquiv.image_source_inter_eq'

added theorem LocalEquiv.image_source_inter_eq

added theorem LocalEquiv.image_symm_image_of_subset_target

added theorem LocalEquiv.image_trans_source

added theorem LocalEquiv.invFun_as_coe

added theorem LocalEquiv.inv_image_trans_target

added theorem LocalEquiv.isImage_source_target

added theorem LocalEquiv.isImage_source_target_of_disjoint

added theorem LocalEquiv.left_inv

added theorem LocalEquiv.map_source

added theorem LocalEquiv.map_target

added theorem LocalEquiv.mem_symm_trans_source

added def LocalEquiv.ofSet

added theorem LocalEquiv.ofSet_coe

added theorem LocalEquiv.ofSet_source

added theorem LocalEquiv.ofSet_symm

added theorem LocalEquiv.ofSet_target

added def LocalEquiv.piecewise

added def LocalEquiv.prod

added theorem LocalEquiv.prod_coe

added theorem LocalEquiv.prod_coe_symm

added theorem LocalEquiv.prod_source

added theorem LocalEquiv.prod_symm

added theorem LocalEquiv.prod_target

added theorem LocalEquiv.prod_trans

added theorem LocalEquiv.refl_coe

added theorem LocalEquiv.refl_prod_refl

added theorem LocalEquiv.refl_restr_source

added theorem LocalEquiv.refl_restr_target

added theorem LocalEquiv.refl_source

added theorem LocalEquiv.refl_symm

added theorem LocalEquiv.refl_target

added theorem LocalEquiv.refl_trans

added theorem LocalEquiv.restr_coe

added theorem LocalEquiv.restr_coe_symm

added theorem LocalEquiv.restr_eq_of_source_subset

added theorem LocalEquiv.restr_source

added theorem LocalEquiv.restr_target

added theorem LocalEquiv.restr_trans

added theorem LocalEquiv.restr_univ

added theorem LocalEquiv.right_inv

added theorem LocalEquiv.source_inter_preimage_inv_preimage

added theorem LocalEquiv.source_inter_preimage_target_inter

added theorem LocalEquiv.source_subset_preimage_target

added theorem LocalEquiv.symm_image_eq_source_inter_preimage

added theorem LocalEquiv.symm_image_image_of_subset_source

added theorem LocalEquiv.symm_image_target_eq_source

added theorem LocalEquiv.symm_image_target_inter_eq'

added theorem LocalEquiv.symm_image_target_inter_eq

added theorem LocalEquiv.symm_mapsTo

added theorem LocalEquiv.symm_piecewise

added theorem LocalEquiv.symm_source

added theorem LocalEquiv.symm_symm

added theorem LocalEquiv.symm_target

added theorem LocalEquiv.target_inter_inv_preimage_preimage

added theorem LocalEquiv.target_subset_preimage_source

added def LocalEquiv.transEquiv

added theorem LocalEquiv.transEquiv_eq_trans

added theorem LocalEquiv.trans_apply

added theorem LocalEquiv.trans_assoc

added theorem LocalEquiv.trans_refl

added theorem LocalEquiv.trans_refl_restr'

added theorem LocalEquiv.trans_refl_restr

added theorem LocalEquiv.trans_self_symm

added theorem LocalEquiv.trans_source''

added theorem LocalEquiv.trans_source'

added theorem LocalEquiv.trans_source

added theorem LocalEquiv.trans_symm_eq_symm_trans_symm

added theorem LocalEquiv.trans_symm_self

added theorem LocalEquiv.trans_target''

added theorem LocalEquiv.trans_target'

added theorem LocalEquiv.trans_target

added structure LocalEquiv

added def mfld_cfg

Modified test/MfldSetTac.lean

deleted theorem LocalEquiv.coe_trans

deleted theorem LocalEquiv.coe_trans_symm

deleted theorem LocalEquiv.left_inv

deleted theorem LocalEquiv.map_source

deleted def LocalEquiv.symm

deleted theorem LocalEquiv.symm_source

deleted def LocalEquiv.trans

deleted theorem LocalEquiv.trans_source

deleted structure LocalEquiv

deleted theorem Set.inter_univ

deleted theorem Set.mem_inter_eq

deleted theorem Set.mem_preimage

deleted theorem Set.mem_set_of_eq

deleted def Set.preimage

deleted theorem Set.preimage_inter

deleted theorem Set.preimage_univ