Add lemma `loop.affine_equiv_surrounds_iff` - 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 `loop.affine_equiv_surrounds_iff` #50

Closed ocfnash closed 2 years ago

ocfnash commented 2 years ago

And use it to de-sorry loops/surrounding.lean