UniqueDiffNear

Stream: mathlib4

[Yury G. Kudryashov]

In many lemmas about iteratedFDerivWithin etc, the "right" assumption is (UPD: fixed) ∀ᶠ x' in 𝓝[s] x, UniqueDiffWithinAt 𝕜 s x'. Should we introduce a name for this predicate?

[Aaron Liu]

Maybe UniqueDiffOnFilter?

[Sébastien Gouëzel]

Isn't it rather ∀ᶠ x' in 𝓝[s] x, UniqueDiffWithinAt 𝕜 s x'?

[Aaron Liu]

I think that's equivalent

[Yury G. Kudryashov]

Aaron Liu said:

I think that's equivalent

No, in the correct version we don't assume that x' \notin s close to x are unique differentiability points of s.

[Aaron Liu]

oh yeah that's not equivalent

[Yury G. Kudryashov]

UPD: it seems that the right one is ∀ᶠ x' in 𝓝[insert x s] x, UniqueDiffWithinAt 𝕜 s x' a.k.a. UniqueDiffWithinAt 𝕜 s x and :up: