Def Homeomorph.toLocalHomeomorph

Modification history

2023-12-11 20:54

Mathlib/Topology/PartialHomeomorph.lean

chore: rename LocalHomeomorph to PartialHomeomorph (#8982) …

Deleted Homeomorph.toLocalHomeomorph View on Github →

2023-07-26 12:12

Mathlib/Topology/LocalHomeomorph.lean

refactor: rename/redefine `homeomorphUnitBall` (#6030) …

Modified Homeomorph.toLocalHomeomorph View on Github →

2023-02-18 19:03

Mathlib/Topology/LocalHomeomorph.lean

feat: port Topology.LocalHomeomorph (#2231)

Added Homeomorph.toLocalHomeomorph View on Github →