mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/normed_space/basic): change `homeomorph_unit_ball` to make it obviously smooth

Open ocfnash opened this issue 2 years ago • 2 comments

Formalized as part of the Sphere Eversion project.

Open in Gitpod

ocfnash avatar Aug 10 '22 16:08 ocfnash

:v: ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Aug 15 '22 08:08 bors[bot]

bors merge

PatrickMassot avatar Aug 15 '22 08:08 PatrickMassot

I'm sorry Sébastien, I didn't see your comment about sqrt before merging.

PatrickMassot avatar Aug 15 '22 09:08 PatrickMassot

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 15 '22 10:08 bors[bot]