Finished proof; Whitney Graustein from sphere eversion pr.

Stream: sphere eversion

[Sam Lindauer]

Hey all, I am not entirely sure if this is the right channel to do this in, but I have recently finished a lean proof where I deduced the Whitney Graustein theorem from the functionality in the sphere eversion project. It currently uses only three extra axioms about turning number, which I plan to reduce to topology based axioms on winding numbers. I have done this under the supervision of @Johan Commelin and Álvaro del pino Gomez. The code can be found at https://github.com/MetalCreator666/WhitneyGraustein

[Patrick Massot]

This is great! This was a long overdue project. I am super busy but I hope I’ll be able to take a look soon.