Add lemma `exists_cont_diff_of_convex₂` and use it to tidy up partition-of-unity argument in reparametrization lemma. - Githubissues

leanprover-community / sphere-eversion

Formalization of the existence of sphere eversions

https://leanprover-community.github.io/sphere-eversion/

Apache License 2.0

36 stars 10 forks source link

Add lemma `exists_cont_diff_of_convex₂` and use it to tidy up partition-of-unity argument in reparametrization lemma. #62

Closed ocfnash closed 2 years ago