Def Homeomorph.transOpenPartialHomeomorph

Modification history

2025-12-09 05:22

Mathlib/Topology/OpenPartialHomeomorph.lean

refactor(Topology/OpenPartialHomeomorph): split long file (#32601)

Modified Homeomorph.transOpenPartialHomeomorph View on Github →

2025-10-02 09:10

Mathlib/Topology/OpenPartialHomeomorph.lean

chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) …

Added Homeomorph.transOpenPartialHomeomorph View on Github →