Commit 2023-07-26 12:12 01335763

View on Github →

refactor: rename/redefine homeomorphUnitBall (#6030)

  • Add Equiv.toLocalEquivOfImageEq and Homeomorph.toLocalHomeomorphOfImageEq.
  • Rename homeomorphUnitBall to Homeomorph.unitBall.
  • Add LocalHomeomorph.univUnitBall, a LocalHomeomorph version of Homeomorph.unitBall.
  • Add LocalHomeomorph.unitBallBall and LocalHomeomorph.univBall. Inspired by a definition from the sphere eversion project.

Estimated changes

modified def Equiv.toLocalEquiv