redefine surrounding_family

Stream: sphere eversion

[Floris van Doorn]

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]

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]

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

[Floris van Doorn]

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