Def LocalHomeomorph.piecewise

Modification history

2023-12-11 20:54

Mathlib/Topology/PartialHomeomorph.lean

chore: rename LocalHomeomorph to PartialHomeomorph (#8982) …

Deleted LocalHomeomorph.piecewise View on Github →

2023-02-18 19:03

Mathlib/Topology/LocalHomeomorph.lean

feat: port Topology.LocalHomeomorph (#2231)

Added LocalHomeomorph.piecewise View on Github →