Local theory

Stream: sphere eversion

[Patrick Massot]

Big sphere eversion project update: Chapters 1 and 2 are now completely sorry-free! This means the local version of flexibility of open and ample differential relations is completely formalized. On paper the remaining step is: "this local statement obviously implies the global statement". I'm cheating slightly because the trick to get parameters for free is only stated globally in the blueprint, so technically we only proved the local statement without parameters. Anyway, the remaining work is 100% about proving the manifold library in mathlib is actually usable.

[Johan Commelin]

Fantastic news!

[Kevin Buzzard]

Congratulations! It will be great to have a serious consumer of the manifold library.