## Stream: sphere eversion

### Topic: redefine surrounding_family

#### Floris van Doorn (Nov 19 2021 at 16:51):

I redefined surrounding_family today. There was a mistake in its definition, since U did not occur in the definition of surrounding_family g b γ U.

According to the blueprint the definition should be

structure surrounding_family (g b : E → F) (γ : E → ℝ → loop F) (U : set E) : Prop :=
(base : ∀ (x ∈ U) (t : ℝ), γ x t 0 = b x)
(t₀ : ∀ (x ∈ U) (s : ℝ), γ x 0 s = b x)
(surrounds : ∀ x ∈ U, (γ x 1).surrounds $g x) (cont : continuous ↿γ)  but I actually redefined it to be structure surrounding_family (g b : E → F) (γ : E → ℝ → loop F) (U : set E) : Prop := (base : ∀ (x : E) (t : ℝ), γ x t 0 = b x) (t₀ : ∀ (x : E) (s : ℝ), γ x 0 s = b x) (surrounds : ∀ x ∈ U, (γ x 1).surrounds$ g x)
(cont : continuous ↿γ)


The difference is that base and t₀ hold for all points in E.
This way, I could reuse the proof of satisfied_or_refund by changing ~12 characters (introducing and using an assumption called hx twice). (Unrelatedly I also refactored the proof of satisfied_or_refund.)
I hope this definition is be fine, since those fields should be easy to satisfy globally. Do you think this will cause problems @Patrick Massot?

#### Patrick Massot (Nov 19 2021 at 20:06):

Of course not mentioning U was a typo. And of course in the traditional way of writing math, everything would be defined only on U. I hope the new version will be convenient but this is purely a formalization question, it has no mathematical content.

#### Patrick Massot (Nov 19 2021 at 20:07):

So I can't answer before trying to use it.

#### Floris van Doorn (Nov 19 2021 at 20:31):

That's reasonable. Let's try it (and I understand that this has no mathematical content).

Last updated: Dec 20 2023 at 11:08 UTC