Commit 2025-10-02 09:10 a50a869e

View on Github →

chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) This PR renames PartialHomeomorph to OpenPartialHomeomorph as discussed in [#mathlib4 > Generalizing `PartialHomeomorph`?](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Generalizing.20.60PartialHomeomorph.60.3F). This is the first step towards generalizing PartialHomeomorph to allow arbitrary sources and targets.

Estimated changes

modified def polarCoord
modified theorem mem_analyticGroupoid
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
added structure OpenPartialHomeomorph
deleted theorem PartialHomeomorph.coe_coe
deleted theorem PartialHomeomorph.mk_coe
deleted structure PartialHomeomorph
added structure OpenPartialHomeomorph
deleted theorem PartialHomeomorph.coe_coe
deleted structure PartialHomeomorph