extend_loops

Stream: sphere eversion

[Floris van Doorn]

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]

I didn't rebuild the website yet.

[Oliver Nash]

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]

Great work Floris!