Zulip Chat Archive

Stream: sphere eversion

Topic: Easy induction on directions


Patrick Massot (Feb 08 2022 at 22:29):

Lemma 2.16 is essentially done modulo the key Lemma 2.11 and some easy sorries. The blueprint describes this as a "straightforward induction using lemma 2.11" but the Lean proof is still 100 lines long and I wanted to have it to make sure the data and properties flow well.

Patrick Massot (Feb 08 2022 at 22:30):

This proof needs cleaning of course, but it shows a lot of things work well.

Patrick Massot (Feb 08 2022 at 22:32):

It also generated quite a few accessible sorries, in case anyone is tired of Lie algebras.


Last updated: Dec 20 2023 at 11:08 UTC