Commit 2026-06-17 17:44 83a621b2

feat: generalize OpenPartialHomeomorph.Defs file to PartialHomeomorph (#39084) Add PartialHomeomorph, which generalises OpenPartialHomoemorph by dropping the condition that the source and target be open. In other words, an OpenPartialHomeomorph is a PartialHomeomorph that additionally has open source and target. This generalisation should find uses for manifolds (extended charts are PartialHomeomorphs, but their target is not open for manifolds with boundary). For CW complexes, we will want a ClosedPartialHomeomorph: this allows re-using results as much as possible. This PR adds the basic definitions; future PRs will add additional material: #39071 indicates what the eventual result may be. Zulip discussion: [#mathlib4 > Generalizing `PartialHomeomorph`?](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Generalizing.20.60PartialHomeomorph.60.3F/with/536896273)