Zulip Chat Archive

Stream: sphere eversion

Topic: extend_loops

Floris van Doorn (Nov 19 2021 at 16:46):

I just finished the proof of extends_loops.

For it, I had to prove the following separation result, which I believe doesn't exist yet

lemma exists_open_between_and_is_compact_closure [locally_compact_space α] [regular_space α]
  {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K  U) :
   V, is_open V  K  V  closure V  U  is_compact (closure V)

Floris van Doorn (Nov 19 2021 at 17:01):

I didn't rebuild the website yet.

Oliver Nash (Nov 19 2021 at 18:33):

Nice work @Floris van Doorn ! For the second week in a row I think I'm about a week away from finishing the proof of lem:smooth_barycentric_coord (definitely close anyway). We're definitely getting somewhere!

Patrick Massot (Nov 19 2021 at 20:03):

Great work Floris!

Last updated: Dec 20 2023 at 11:08 UTC