|
|
|
|
|
|
by ocfnash
734 days ago
|
|
|
If you are curious, I encourage you to look up The Sphere Eversion Project [1]. It was a project in which we formalised a version of Gromov's (open, ample) h-principle for first order differential relations. Part of the reason it was carried out was to demonstrate what is involved formalising something in differential topology. 1. https://leanprover-community.github.io/sphere-eversion/ |
|
|