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):
Great!
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):
Yes.
Last updated: Dec 20 2023 at 11:08 UTC