Zulip Chat Archive

We have lemmas that require that two sets coincide locally with the assumption 𝓝[s] x = 𝓝[t] x, like docs#continuousWithinAt_congr_nhds, and others with the assumption s =ᶠ[𝓝 x] t like docs#hasFDerivWithinAt_congr_set. These two assumptions are equivalent, thanks to docs#nhdsWithin_eq_iff_eventuallyEq, so we should choose a normal form. I'd rather go for s =ᶠ[𝓝 x] t(because it admits the nice weakening s =ᶠ[𝓝[{y}ᶜ] x] t which shows up in some versions like docs#hasFDerivWithinAt_congr_set') and deprecate the other form. Any thought on that?

Anatole Dedecker (Oct 18 2024 at 13:28):

I would go with the second one, I think it reads better.

Yaël Dillies (Oct 18 2024 at 13:29):

There is also one less x appearing in it

Eric Wieser (Oct 18 2024 at 13:32):

s =ᶠ[𝓝 x] t is abusing the set/function defeq, right?

Sébastien Gouëzel (Oct 18 2024 at 13:37):

Yes, it's abusing defeqs. That's the only reason that could make me hesitate a little bit here.

Vincent Beffara (Oct 18 2024 at 13:40):

There is also the spelling (· ∈ s) =ᶠ[𝓝 x] (· ∈ t) which is a bit hevier but does not abuse defeqs.

Anatole Dedecker (Oct 18 2024 at 13:40):

I think we're already using this one quite a lot in measure theory, right?

Eric Wieser (Oct 18 2024 at 13:46):

Probably we should find the old thread about defeqs rather than rehashing it here, cc @Yury G. Kudryashov who I think started it

Yury G. Kudryashov (Oct 18 2024 at 15:12):

I'll find the old thread soon. I think that we should go with s =ᶠ[𝓝 x] t and add an issue to do something about the defeq abuse.

Yury G. Kudryashov (Oct 18 2024 at 15:14):

Possible solutions to the defeq abuse are (a) add a set-specific notation that unfolds to (· ∈ s) =ᶠ[𝓝 x] (· ∈ t); (b) turn Set _ into a one-field structure with coercion to function given by (· ∈ s).