# Zulip Chat Archive

## 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