Commit 2023-12-13 09:43 f7006a73

View on Github →

chore: rename LocalEquiv to PartialEquiv (#8984) The current name is misleading: there's no open set involved; it's just an equivalence between subsets of domain and target. zulip discussion PEquiv is similarly named: this is fine, as they're different designs for the same concept.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

deleted def ApproximatesLinearOn.toLocalEquiv

added def ApproximatesLinearOn.toPartialEquiv

Modified Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

Modified Mathlib/Data/PEquiv.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Product.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/Geometry/Manifold/MFDeriv.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

modified theorem ModelWithCorners.mk_coe

modified theorem ModelWithCorners.mk_symm

deleted theorem ModelWithCorners.toLocalEquiv_coe

deleted theorem ModelWithCorners.toLocalEquiv_coe_symm

added theorem ModelWithCorners.toPartialEquiv_coe

added theorem ModelWithCorners.toPartialEquiv_coe_symm

modified def PartialHomeomorph.extend

modified def extChartAt

modified theorem extChartAt_model_space_eq_id

modified theorem modelWithCornersSelf_localEquiv

deleted theorem modelWithCorners_prod_toLocalEquiv

added theorem modelWithCorners_prod_toPartialEquiv

Modified Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

deleted theorem TangentBundle.chartAt_toLocalEquiv

added theorem TangentBundle.chartAt_toPartialEquiv

Renamed Mathlib/Logic/Equiv/LocalEquiv.lean to Mathlib/Logic/Equiv/PartialEquiv.lean

deleted theorem Equiv.refl_toLocalEquiv

added theorem Equiv.refl_toPartialEquiv

deleted theorem Equiv.symm_toLocalEquiv

added theorem Equiv.symm_toPartialEquiv

deleted def Equiv.toLocalEquiv

deleted def Equiv.toLocalEquivOfImageEq

added def Equiv.toPartialEquiv

added def Equiv.toPartialEquivOfImageEq

deleted def Equiv.transLocalEquiv

deleted theorem Equiv.transLocalEquiv_eq_trans

added def Equiv.transPartialEquiv

added theorem Equiv.transPartialEquiv_eq_trans

deleted theorem Equiv.trans_toLocalEquiv

added theorem Equiv.trans_toPartialEquiv

deleted theorem LocalEquiv.EqOnSource.eqOn

deleted theorem LocalEquiv.EqOnSource.restr

deleted theorem LocalEquiv.EqOnSource.source_eq

deleted theorem LocalEquiv.EqOnSource.source_inter_preimage_eq

deleted theorem LocalEquiv.EqOnSource.symm'

deleted theorem LocalEquiv.EqOnSource.symm_eqOn

deleted theorem LocalEquiv.EqOnSource.target_eq

deleted theorem LocalEquiv.EqOnSource.trans'

deleted def LocalEquiv.EqOnSource

deleted theorem LocalEquiv.IsImage.apply_mem_iff

deleted theorem LocalEquiv.IsImage.iff_preimage_eq

deleted theorem LocalEquiv.IsImage.iff_symm_preimage_eq

deleted theorem LocalEquiv.IsImage.image_eq

deleted theorem LocalEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn

deleted theorem LocalEquiv.IsImage.leftInvOn_piecewise

deleted theorem LocalEquiv.IsImage.of_image_eq

deleted theorem LocalEquiv.IsImage.of_symm_image_eq

deleted def LocalEquiv.IsImage.restr

deleted theorem LocalEquiv.IsImage.symm_apply_mem_iff

deleted theorem LocalEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn

deleted theorem LocalEquiv.IsImage.symm_iff

deleted theorem LocalEquiv.IsImage.symm_image_eq

deleted theorem LocalEquiv.IsImage.symm_mapsTo

deleted def LocalEquiv.IsImage

deleted def LocalEquiv.Simps.symm_apply

deleted theorem LocalEquiv.coe_symm_mk

deleted theorem LocalEquiv.coe_trans

deleted theorem LocalEquiv.coe_trans_symm

deleted def LocalEquiv.copy

deleted theorem LocalEquiv.copy_eq

deleted def LocalEquiv.disjointUnion

deleted theorem LocalEquiv.disjointUnion_eq_piecewise

deleted theorem LocalEquiv.eqOnSource_refl

deleted theorem LocalEquiv.eq_of_eqOnSource_univ

deleted theorem LocalEquiv.eq_symm_apply

deleted theorem LocalEquiv.exists_mem_target

deleted theorem LocalEquiv.forall_mem_target

deleted theorem LocalEquiv.image_eq_target_inter_inv_preimage

deleted theorem LocalEquiv.image_source_eq_target

deleted theorem LocalEquiv.image_source_inter_eq'

deleted theorem LocalEquiv.image_source_inter_eq

deleted theorem LocalEquiv.image_symm_image_of_subset_target

deleted theorem LocalEquiv.image_trans_source

deleted theorem LocalEquiv.invFun_as_coe

deleted theorem LocalEquiv.inv_image_trans_target

deleted theorem LocalEquiv.isImage_source_target

deleted theorem LocalEquiv.isImage_source_target_of_disjoint

deleted theorem LocalEquiv.left_inv

deleted theorem LocalEquiv.map_source''

deleted theorem LocalEquiv.map_source

deleted theorem LocalEquiv.map_target

deleted theorem LocalEquiv.mem_symm_trans_source

deleted def LocalEquiv.ofSet

deleted theorem LocalEquiv.ofSet_coe

deleted theorem LocalEquiv.ofSet_source

deleted theorem LocalEquiv.ofSet_symm

deleted theorem LocalEquiv.ofSet_target

deleted theorem LocalEquiv.pi_refl

deleted theorem LocalEquiv.pi_symm

deleted theorem LocalEquiv.pi_symm_apply

deleted theorem LocalEquiv.pi_trans

deleted def LocalEquiv.piecewise

deleted def LocalEquiv.prod

deleted theorem LocalEquiv.prod_coe

deleted theorem LocalEquiv.prod_coe_symm

deleted theorem LocalEquiv.prod_source

deleted theorem LocalEquiv.prod_symm

deleted theorem LocalEquiv.prod_target

deleted theorem LocalEquiv.prod_trans

deleted theorem LocalEquiv.refl_coe

deleted theorem LocalEquiv.refl_prod_refl

deleted theorem LocalEquiv.refl_restr_source

deleted theorem LocalEquiv.refl_restr_target

deleted theorem LocalEquiv.refl_source

deleted theorem LocalEquiv.refl_symm

deleted theorem LocalEquiv.refl_target

deleted theorem LocalEquiv.refl_trans

deleted theorem LocalEquiv.restr_coe

deleted theorem LocalEquiv.restr_coe_symm

deleted theorem LocalEquiv.restr_eq_of_source_subset

deleted theorem LocalEquiv.restr_source

deleted theorem LocalEquiv.restr_target

deleted theorem LocalEquiv.restr_trans

deleted theorem LocalEquiv.restr_univ

deleted theorem LocalEquiv.right_inv

deleted theorem LocalEquiv.source_inter_preimage_inv_preimage

deleted theorem LocalEquiv.source_inter_preimage_target_inter

deleted theorem LocalEquiv.source_subset_preimage_target

deleted theorem LocalEquiv.symm_bijective

deleted theorem LocalEquiv.symm_image_eq_source_inter_preimage

deleted theorem LocalEquiv.symm_image_image_of_subset_source

deleted theorem LocalEquiv.symm_image_target_eq_source

deleted theorem LocalEquiv.symm_image_target_inter_eq'

deleted theorem LocalEquiv.symm_image_target_inter_eq

deleted theorem LocalEquiv.symm_mapsTo

deleted theorem LocalEquiv.symm_piecewise

deleted theorem LocalEquiv.symm_source

deleted theorem LocalEquiv.symm_symm

deleted theorem LocalEquiv.symm_target

deleted theorem LocalEquiv.target_inter_inv_preimage_preimage

deleted theorem LocalEquiv.target_subset_preimage_source

deleted def LocalEquiv.transEquiv

deleted theorem LocalEquiv.transEquiv_eq_trans

deleted theorem LocalEquiv.trans_apply

deleted theorem LocalEquiv.trans_assoc

deleted theorem LocalEquiv.trans_ofSet

deleted theorem LocalEquiv.trans_refl

deleted theorem LocalEquiv.trans_refl_restr'

deleted theorem LocalEquiv.trans_refl_restr

deleted theorem LocalEquiv.trans_self_symm

deleted theorem LocalEquiv.trans_source''

deleted theorem LocalEquiv.trans_source'

deleted theorem LocalEquiv.trans_source

deleted theorem LocalEquiv.trans_symm_eq_symm_trans_symm

deleted theorem LocalEquiv.trans_symm_self

deleted theorem LocalEquiv.trans_target''

deleted theorem LocalEquiv.trans_target'

deleted theorem LocalEquiv.trans_target

deleted structure LocalEquiv

added theorem PartialEquiv.EqOnSource.eqOn

added theorem PartialEquiv.EqOnSource.restr

added theorem PartialEquiv.EqOnSource.source_eq

added theorem PartialEquiv.EqOnSource.source_inter_preimage_eq

added theorem PartialEquiv.EqOnSource.symm'

added theorem PartialEquiv.EqOnSource.symm_eqOn

added theorem PartialEquiv.EqOnSource.target_eq

added theorem PartialEquiv.EqOnSource.trans'

added def PartialEquiv.EqOnSource

added theorem PartialEquiv.IsImage.apply_mem_iff

added theorem PartialEquiv.IsImage.iff_preimage_eq

added theorem PartialEquiv.IsImage.iff_symm_preimage_eq

added theorem PartialEquiv.IsImage.image_eq

added theorem PartialEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn

added theorem PartialEquiv.IsImage.leftInvOn_piecewise

added theorem PartialEquiv.IsImage.of_image_eq

added theorem PartialEquiv.IsImage.of_symm_image_eq

added def PartialEquiv.IsImage.restr

added theorem PartialEquiv.IsImage.symm_apply_mem_iff

added theorem PartialEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn

added theorem PartialEquiv.IsImage.symm_iff

added theorem PartialEquiv.IsImage.symm_image_eq

added theorem PartialEquiv.IsImage.symm_mapsTo

added def PartialEquiv.IsImage

added def PartialEquiv.Simps.symm_apply

added theorem PartialEquiv.coe_symm_mk

added theorem PartialEquiv.coe_trans

added theorem PartialEquiv.coe_trans_symm

added def PartialEquiv.copy

added theorem PartialEquiv.copy_eq

added def PartialEquiv.disjointUnion

added theorem PartialEquiv.disjointUnion_eq_piecewise

added theorem PartialEquiv.eqOnSource_refl

added theorem PartialEquiv.eq_of_eqOnSource_univ

added theorem PartialEquiv.eq_symm_apply

added theorem PartialEquiv.exists_mem_target

added theorem PartialEquiv.forall_mem_target

added theorem PartialEquiv.image_eq_target_inter_inv_preimage

added theorem PartialEquiv.image_source_eq_target

added theorem PartialEquiv.image_source_inter_eq'

added theorem PartialEquiv.image_source_inter_eq

added theorem PartialEquiv.image_symm_image_of_subset_target

added theorem PartialEquiv.image_trans_source

added theorem PartialEquiv.invFun_as_coe

added theorem PartialEquiv.inv_image_trans_target

added theorem PartialEquiv.isImage_source_target

added theorem PartialEquiv.isImage_source_target_of_disjoint

added theorem PartialEquiv.left_inv

added theorem PartialEquiv.map_source''

added theorem PartialEquiv.map_source

added theorem PartialEquiv.map_target

added theorem PartialEquiv.mem_symm_trans_source

added def PartialEquiv.ofSet

added theorem PartialEquiv.ofSet_coe

added theorem PartialEquiv.ofSet_source

added theorem PartialEquiv.ofSet_symm

added theorem PartialEquiv.ofSet_target

added theorem PartialEquiv.pi_refl

added theorem PartialEquiv.pi_symm

added theorem PartialEquiv.pi_symm_apply

added theorem PartialEquiv.pi_trans

added def PartialEquiv.piecewise

added def PartialEquiv.prod

added theorem PartialEquiv.prod_coe

added theorem PartialEquiv.prod_coe_symm

added theorem PartialEquiv.prod_source

added theorem PartialEquiv.prod_symm

added theorem PartialEquiv.prod_target

added theorem PartialEquiv.prod_trans

added theorem PartialEquiv.refl_coe

added theorem PartialEquiv.refl_prod_refl

added theorem PartialEquiv.refl_restr_source

added theorem PartialEquiv.refl_restr_target

added theorem PartialEquiv.refl_source

added theorem PartialEquiv.refl_symm

added theorem PartialEquiv.refl_target

added theorem PartialEquiv.refl_trans

added theorem PartialEquiv.restr_coe

added theorem PartialEquiv.restr_coe_symm

added theorem PartialEquiv.restr_eq_of_source_subset

added theorem PartialEquiv.restr_source

added theorem PartialEquiv.restr_target

added theorem PartialEquiv.restr_trans

added theorem PartialEquiv.restr_univ

added theorem PartialEquiv.right_inv

added theorem PartialEquiv.source_inter_preimage_inv_preimage

added theorem PartialEquiv.source_inter_preimage_target_inter

added theorem PartialEquiv.source_subset_preimage_target

added theorem PartialEquiv.symm_bijective

added theorem PartialEquiv.symm_image_eq_source_inter_preimage

added theorem PartialEquiv.symm_image_image_of_subset_source

added theorem PartialEquiv.symm_image_target_eq_source

added theorem PartialEquiv.symm_image_target_inter_eq'

added theorem PartialEquiv.symm_image_target_inter_eq

added theorem PartialEquiv.symm_mapsTo

added theorem PartialEquiv.symm_piecewise

added theorem PartialEquiv.symm_source

added theorem PartialEquiv.symm_symm

added theorem PartialEquiv.symm_target

added theorem PartialEquiv.target_inter_inv_preimage_preimage

added theorem PartialEquiv.target_subset_preimage_source

added def PartialEquiv.transEquiv

added theorem PartialEquiv.transEquiv_eq_trans

added theorem PartialEquiv.trans_apply

added theorem PartialEquiv.trans_assoc

added theorem PartialEquiv.trans_ofSet

added theorem PartialEquiv.trans_refl

added theorem PartialEquiv.trans_refl_restr'

added theorem PartialEquiv.trans_refl_restr

added theorem PartialEquiv.trans_self_symm

added theorem PartialEquiv.trans_source''

added theorem PartialEquiv.trans_source'

added theorem PartialEquiv.trans_source

added theorem PartialEquiv.trans_symm_eq_symm_trans_symm

added theorem PartialEquiv.trans_symm_self

added theorem PartialEquiv.trans_target''

added theorem PartialEquiv.trans_target'

added theorem PartialEquiv.trans_target

added structure PartialEquiv

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/Topology/Covering.lean

Modified Mathlib/Topology/FiberBundle/Basic.lean

deleted def FiberBundleCore.localTrivAsLocalEquiv

deleted theorem FiberBundleCore.localTrivAsLocalEquiv_apply

deleted theorem FiberBundleCore.localTrivAsLocalEquiv_coe

deleted theorem FiberBundleCore.localTrivAsLocalEquiv_source

deleted theorem FiberBundleCore.localTrivAsLocalEquiv_symm

deleted theorem FiberBundleCore.localTrivAsLocalEquiv_target

deleted theorem FiberBundleCore.localTrivAsLocalEquiv_trans

added def FiberBundleCore.localTrivAsPartialEquiv

added theorem FiberBundleCore.localTrivAsPartialEquiv_apply

added theorem FiberBundleCore.localTrivAsPartialEquiv_coe

added theorem FiberBundleCore.localTrivAsPartialEquiv_source

added theorem FiberBundleCore.localTrivAsPartialEquiv_symm

added theorem FiberBundleCore.localTrivAsPartialEquiv_target

added theorem FiberBundleCore.localTrivAsPartialEquiv_trans

deleted theorem FiberBundleCore.mem_localTrivAsLocalEquiv_source

deleted theorem FiberBundleCore.mem_localTrivAsLocalEquiv_target

added theorem FiberBundleCore.mem_localTrivAsPartialEquiv_source

added theorem FiberBundleCore.mem_localTrivAsPartialEquiv_target

modified theorem FiberBundleCore.open_source'

Modified Mathlib/Topology/FiberBundle/Constructions.lean

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

modified theorem Pretrivialization.apply_symm_apply

modified theorem Pretrivialization.coe_coe

modified theorem Pretrivialization.ext'

modified theorem Pretrivialization.proj_symm_apply

modified theorem Pretrivialization.symm_apply_apply

deleted theorem Pretrivialization.toLocalEquiv_injective

added theorem Pretrivialization.toPartialEquiv_injective

modified structure Pretrivialization

Modified Mathlib/Topology/IsLocalHomeomorph.lean

Modified Mathlib/Topology/PartialHomeomorph.lean

deleted theorem PartialHomeomorph.IsImage.toLocalEquiv

added theorem PartialHomeomorph.IsImage.toPartialEquiv

modified theorem PartialHomeomorph.coe_coe

modified theorem PartialHomeomorph.coe_coe_symm

modified theorem PartialHomeomorph.eq_of_localEquiv_eq

modified theorem PartialHomeomorph.mk_coe

modified theorem PartialHomeomorph.mk_coe_symm

modified def PartialHomeomorph.ofContinuousOpen

modified def PartialHomeomorph.ofContinuousOpenRestrict

deleted theorem PartialHomeomorph.ofSet_toLocalEquiv

added theorem PartialHomeomorph.ofSet_toPartialEquiv

modified theorem PartialHomeomorph.refl_localEquiv

modified def PartialHomeomorph.replaceEquiv

modified theorem PartialHomeomorph.replaceEquiv_eq_self

deleted theorem PartialHomeomorph.restrOpen_toLocalEquiv

added theorem PartialHomeomorph.restrOpen_toPartialEquiv

deleted theorem PartialHomeomorph.restr_toLocalEquiv'

deleted theorem PartialHomeomorph.restr_toLocalEquiv

added theorem PartialHomeomorph.restr_toPartialEquiv'

added theorem PartialHomeomorph.restr_toPartialEquiv

deleted theorem PartialHomeomorph.symm_toLocalEquiv

added theorem PartialHomeomorph.symm_toPartialEquiv

deleted theorem PartialHomeomorph.toLocalEquiv_injective

added theorem PartialHomeomorph.toPartialEquiv_injective

deleted theorem PartialHomeomorph.trans_toLocalEquiv

added theorem PartialHomeomorph.trans_toPartialEquiv

Modified Mathlib/Topology/VectorBundle/Hom.lean

Modified scripts/style-exceptions.txt

Modified test/MfldSetTac.lean

modified def ModelWithCorners.symm

modified structure ModelWithCorners

deleted theorem PartialHomeomorph.symm_to_LocalEquiv

added theorem PartialHomeomorph.symm_to_PartialEquiv

modified structure PartialHomeomorph