sup/Sup

Stream: mathlib4

[Yaël Dillies]

Patrick Massot said:

I went with sup supₛ supᵢ inf infₛ infᵢ

Could we partially step back on this decision? It's really hard for me to visually distinguish supₛ from supᵢ. My brain parses both as "sup + small squiggle". It would be much easier if supr and infi kept their original name, which would make the set of names be

sup supₛ supr
inf infₛ infi

[Eric Wieser]

I agree, these are pretty terrible for readability

[Yaël Dillies]

To exemplify, here's how it looks like on Zulip browser and in VScode

[Jireh Loreaux]

But what about union? How do we name that?

[Eric Wieser]

Some other disadvantages of the new spelling:

• It's hard to search for lemmas about infᵢ in the web docs, unless you have a system-wide input mechanism or the string in your clipboard. We could consider enhancing the doc-gen search field to fix this
• It doesn't work with Zulip Linkifiers, docs4#infᵢ
• It's odd having \infi as a shortcut for the notation for \inf\_i

[Yaël Dillies]

Another suggestion is

sup supS supI
inf infS infI

or

sup sSup iSup
inf sInf iInf

[Yaël Dillies]

I quite like this last suggestion because it matches our existing mathlib conventions around bUnion, uIcc, cIcc, pnat of putting modifiers as one-letter prefixes. It also has the slight advantage of making big operators have a cap to their name.

[Mario Carneiro]

yup, I'm strongly opposed to the new name and my original vote was basically "anything but that". We use unicode very rarely in label names and I've always found it to be bad for readability.

[Yaël Dillies]

Uh oh, it is huge: !4#3938

[Kevin Buzzard]

$2^7\times 3$ files changed!

[Scott Morrison]

I've hit merge on this, on the principle that it is a lot of work to do these renames, and Yaël has done it, and we shouldn't let it rot. Further bikeshedding postponed until the next naming committee meeting. :-)

[Notification Bot]

This topic was moved here from #lean4 > sup/Sup by Eric Wieser.