RFC: notation for `WithTop ℕ∞`

Stream: mathlib4

[Ben Eltschig]

Throughout analysis and differential geometry in mathlib, we currently make heavy use of WithTop ℕ∞ as the type of smoothness degrees for e.g. the ContDiff API. We have notation ∞ for (⊤ : ℕ∞) : WithTop ℕ∞ and ω for ⊤ : WithTop ℕ∞, but currently no notation for WithTop ℕ∞ itself. I propose introducting notation ℕ∞ω for this, analogous to the notation ℕ∞ we already have for ENat. I've opened a draft PR for this at #34649.

What do you think of this? Would this notation make sense to add, and if so, how should it be scoped? The existing notations ∞ and ω are scoped to the ContDiff namespace (and rightfully so, since ∞ might denote terms of different types in other contexts), but while creating the PR I noticed that many files that mention WithTop ℕ∞ currently don't open ContDiff because they have have no need to mention ∞ and ω specifically and just work with general n : WithTop ℕ∞. I'm wondering if that would be reason enough to make ℕ∞ω available globally, since there is presumably no risk of it meaning something different in other contexts like with ∞ and ω.

[Michael Rothgang]

Thanks for trying to make working in calculus and manifolds more ergonomic. I appreciate the effort; we need to keep trying harder at this. That said: can you say more about this particular proposal, please? What's your motivation, just brevity?

My first impression, certainly not well-thought-out, is that I'm not sure if the new notation is worth it. We add one more abbreviation which is non-standard and needs to be learned, in return for a few characters. I will think about it more; it's possible my opinion will be different then.

[Snir Broshi]

Michael Rothgang said:

We add one more abbreviation which is non-standard and needs to be learned

FWIW as a newcomer a double WithBot was a little confusing to me; when I saw WithBot ℕ∞ I assumed I just read WithBot ℕ or ℕ∞, I didn't notice the WithBot was actually doubled. I think the suggestion might make it more obvious that something new is going on since there's an ω in it, though it could still be easily mistaken for ℕ∞.
But I think ∞ vs ω as terms of N∞ω is confusing since I can't immediately tell which is bigger. It might be fine for people who are more used to the $C^\omega$ / $C^\infty$ notation, but my instinct was to think in terms of ordinals and cardinals.

[Ben Eltschig]

Michael Rothgang said:

That said: can you say more about this particular proposal, please? What's your motivation, just brevity?

Brevity is one thing, but I also feel like this would fill a lexical gap we currently have - we already have notation for other types of extended numbers like ℕ∞ and ℝ≥0∞ after all, as well as the notation ω for ⊤ : WithTop ℕ∞, so calling WithTop ℕ∞ ℕ∞ω seems very natural / fitting to me. I understand the concern about this being yet another notation that one has to learn, but arguably n : WithTop ℕ∞ already isn't very intuitive when one first sees it: introducing a notation for it would even have the advantage of allowing us to add a docstring, whereas if one sees WithTop ℕ∞ currently the only docstrings available on hover are those of WithTop and ℕ∞, which don't really explain why we're adding a top element to a type that already has one.

[Yury G. Kudryashov]

One advantage of having this notation is that it comes with a docstring.

[Ben Eltschig]

I just remembered this PR / thread - since the message with the most thumbs up in this thread is about an advantage this notation would bring, I take that as a sign it is indeed a welcome addition. That leaves open the question of whether it should be scoped or not not. Should that also be discussed here, or should further discussion happen on github on the PR?

[Yury G. Kudryashov]

AFAIK, ω in this context makes sense only for C^k, so I would make it scoped.

[Ben Eltschig]

The argument for having it globally is that a lot more files mention WithTop ℕ∞than ω, so if we make the notation scoped we could either not use it everywhere or would have to add open scoped ContDiff to a lot of files that currently don't have it

[Ben Eltschig]

but I agree that it would be a bit weird to have ℕ∞ω available in contexts where ω is not

[Ben Eltschig]

out of the two options of using the notation only in some files and adding open scoped ContDiff to a lot of files, which one would be preferred?