Zulip Chat Archive

Stream: sphere eversion

Topic: Lemma 2.13

Anatole Dedecker (Oct 24 2021 at 13:55):

@Bhavik Mehta Do you intend to continue your old work on lemma 2.13 (ampleness of complements, as you called it in your PR) ? I'd like to work on it, but I won't if you still want to do it.

Bhavik Mehta (Oct 24 2021 at 14:10):

Feel free to take it over!

Anatole Dedecker (Oct 27 2021 at 20:07):

I've opened https://github.com/leanprover-community/sphere-eversion/pull/34 with a sorry-free proof of lemma 2.13, but it still needs a lot of cleaning.

Patrick Massot (Oct 27 2021 at 20:09):


Anatole Dedecker (Dec 20 2021 at 23:52):

It's been a long time, but I'd say this PR is now ready for review, appart from a few auxiliary lemmas remaining which I PR-ed to mathlib but are not merged yet.

Patrick Massot (Dec 21 2021 at 16:43):

This Lemma 2.13 is now merged and green on the dependency graph! Many thanks to Anatole for this nice contribution to the project!

Patrick Massot (Dec 21 2021 at 16:45):

This is a nice milestone because it's a very geometric statement that nobody would want to formally prove unless cornered by a proof assistant.

Patrick Massot (Dec 21 2021 at 16:47):

It says that, in a real vector space, the convex hull of any connected component of the complement of a linear subspace with codimension at least 2 has full convex hull.

Oliver Nash (Dec 21 2021 at 17:02):

Nice work @Anatole Dedecker this is the first Section 2 ellipse to turn green :-)

Yaël Dillies (Dec 21 2021 at 17:14):

What does the blue surrounding really mean? Surely sphere_eversion isn't ready yet?

Patrick Massot (Dec 21 2021 at 17:16):

The statement is ready to be formalized. It doesn't depend on any definition from the blueprint that hasn't been formalized.

Yaël Dillies (Dec 21 2021 at 17:17):

Oh I see! That's not something you can tell from the dependency graph, because it does depend on unformalized definitions.

Patrick Massot (Dec 21 2021 at 17:29):

Yes, we could actually add definitions to the blueprint and it wouldn't be blue anymore.

Patrick Massot (Dec 22 2021 at 11:18):

Anatole, I didn't move any of your lemmas in to_mathlib, but I think everything about connectedness of complements should be PRed to mathlib. Only the convex hull stuff is too specialized for mathlib.

Yaël Dillies (Dec 22 2021 at 12:39):

Ah! I would have said the convex hull results were worth having.

Patrick Massot (Dec 22 2021 at 13:11):

Maybe we can leave the ampleness condition in the project but put the convex hull computation in mathlib.

Anatole Dedecker (Dec 22 2021 at 14:04):

Ok I'll PR it. We should still keep the part of the proof that goes to mathlib in the blueprint right ?

Patrick Massot (Dec 22 2021 at 14:08):


Last updated: Dec 20 2023 at 11:08 UTC