Commit 2023-12-11 20:54 bbc6e56d

View on Github →

chore: rename LocalHomeomorph to PartialHomeomorph (#8982) LocalHomeomorph evokes a "local homeomorphism": this is not what this means. Instead, this is a homeomorphism on an open set of the domain (extended to the whole space, by the junk value pattern). Hence, partial homeomorphism is more appropriate, and avoids confusion with IsLocallyHomeomorph. A future PR will rename LocalEquiv to PartialEquiv. Zulip discussion

Estimated changes

modified def polarCoord
modified theorem StructureGroupoid.id_mem
modified theorem StructureGroupoid.locality
modified theorem StructureGroupoid.symm
modified theorem StructureGroupoid.trans
modified theorem chartedSpaceSelf_atlas
modified theorem coe_achart
modified theorem hasGroupoid_of_pregroupoid
modified theorem mem_groupoid_of_pregroupoid
modified theorem mem_maximalAtlas_iff
modified def stereographic
modified theorem Trivialization.coe_coe
modified theorem Trivialization.coe_mk
modified theorem Trivialization.ext'
modified theorem Trivialization.map_target
modified structure Trivialization
modified theorem IsLocalHomeomorph.mk
modified theorem IsLocalHomeomorphOn.mk
deleted theorem LocalHomeomorph.coe_coe
deleted theorem LocalHomeomorph.coe_trans
deleted theorem LocalHomeomorph.left_inv
deleted theorem LocalHomeomorph.mk_coe
deleted def LocalHomeomorph.pi
deleted theorem LocalHomeomorph.prod_symm
deleted theorem LocalHomeomorph.refl_symm
deleted theorem LocalHomeomorph.right_inv
deleted theorem LocalHomeomorph.symm_symm
deleted structure LocalHomeomorph
added structure PartialHomeomorph
deleted theorem LocalHomeomorph.coe_coe
deleted theorem LocalHomeomorph.left_inv
deleted structure LocalHomeomorph
added structure PartialHomeomorph