naming convention: `𝓝[≥] a` etc

Stream: mathlib4

[Yury G. Kudryashov]

Currently, lemmas about 𝓝[≥] a, 𝓝[>] a etc use different naming conventions:

• nhdsWithin_Ici/nhdsWithin_Ioi
• nhdsWithin_right (no consistent way to tell ≥ from >)

What should we do about it?

[Yury G. Kudryashov]

/poll Name for lemmas about 𝓝[≥] a, 𝓝[>] a
nhdsWithin_Ici, nhdsWithin_Ioi
nhdsWithin_right, nhdsWithin_right
nhdsWithin_right, nhdsWithin_right'
nhdsGE, nhdsGT

[Yury G. Kudryashov]

/poll Name for a lemma about 𝓝[≠] a
punctured_nhds
nhdsWithin_compl_singleton
nhdsNE

[Yury G. Kudryashov]

I've started #20188

[Yury G. Kudryashov]

I consider #20188 ready for review now. I didn't rename all lemmas about 𝓝[≥] a, but I would prefer to merge this and prepare a new PR later this week.

[Eric Wieser]

Can we update the docstring for docs#nhdsWithin to enumerate these naming conventions?

[Yury G. Kudryashov]

I can submit a PR later today.

[Yury G. Kudryashov]

BTW, How can I find all non-deprecated theorems about 𝓝[≥] a to see if any of them should be renamed? AFAICS, Loogle has no option to hide deprecated theorems.

[Eric Wieser]

You could use the loogle API locally

[Yury G. Kudryashov]

How do I find out if a theorem is deprecated?

[Eric Wieser]

I would guess some digging in the implementation of the attribute will reveal an environment extension

[Yury G. Kudryashov]

I'll have a look tomorrow.

[Violeta Hernández]

As someone who's new to this part of Mathlib, thanks for this! It's not at all obvious that this involves intervals nor nhdsWithin from either the notation or the docstring.