Def LocalHomeomorph.unitBallBall

Modification history

2023-12-11 20:54

Mathlib/Analysis/NormedSpace/HomeomorphBall.lean

chore: rename LocalHomeomorph to PartialHomeomorph (#8982) …

Deleted LocalHomeomorph.unitBallBall View on Github →

2023-07-26 12:12

Mathlib/Analysis/NormedSpace/HomeomorphBall.lean

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

Added LocalHomeomorph.unitBallBall View on Github →