Notation for superscript infinity

Stream: mathlib4

[Dean Young]

Superscript infinity (${}^{\infty}$) is not in the unicode catalogue. But sometimes VS Code has something of its own. Does anyone know if there is a superscript infinity feature? I would really enjoy that.

[Yury G. Kudryashov]

Even if VS Code supports some non-standard glyph, please don't push it to Mathlib. There are people who

• read the code in a browser;
• use Emacs or NeoVim

[Dean Young]

@Yury G. Kudryashov my bad, thanks for this

[Kyle Miller]

sometimes VS Code has something of its own

What's an example of that?

[Dean Young]

I just saw on about 1/4th from Eric Wieser, but I can't seem to find it.

[Eric Wieser]

That's not an example of this

[Eric Wieser]

Vscode can only display unicode characters (because that is what are stored in text files) that are in a font on your system (because that is how it knows to draw them)

[Eric Wieser]

Unicode has a"private use" space with unassigned characters that you can display however you like in a custom font, but I think this is what @Yury G. Kudryashov is saying is a really bad idea

[Julian Berman]

Note also that there is a combining infinity character -- https://www.fileformat.info/info/unicode/char/1ab2/browsertest.htm -- though if you see the font support page, basically nothing has it.

[Eric Wieser]

X᪲ (X᪲)

[Eric Wieser]

Apparently for German dialectology, so presumably not something the unicode consortium would like being used for mathematics!

[Dean Young]

The Unicode Technical Committee (UTC) has Microsoft as a member. Maybe eventually someone can pool some character requests.

https://www.unicode.org/consortium/distlist.html
https://home.unicode.org/membership/membership-levels/

[Julian Berman]

FWIW anyone can submit proposals for new characters -- that's here https://www.unicode.org/pending/proposals.html and the pipeline of proposed new characters is https://www.unicode.org/alloc/Pipeline.html though I'm not sure what the philosophical preference is these days vis a vis combining characters vs standalone, I thought it was that there still was a preference to have both versions but it seems not for this.

[Dean Young]

@Julian Berman Thanks. Do you think there are other characters people might want besides this?

[Dean Young]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Best.20lim.20in.20unicode.3F

[Dean Young]

So the top two for me are superscript infinity and a nice looking left and right limit.

[Dean Young]

Beyond that, there's the missing superscript and subscript characters and how ℂ and ℚ look different.

[Dean Young]

Screenshot-2024-06-03-at-1.17.41PM.png

[Dean Young]

Screenshot-2024-06-03-at-1.21.55PM.png

[Eric Wieser]

You might want to read https://stackoverflow.com/a/76617653

[Eric Wieser]

In short, unicode is not intended to represent arbitrary rich text. If you really want these things, you could create a font with a custom ligature that renders lim-> as your image above, but this Zulip is a poor place to discuss that

[Eric Wieser]

Dean Young said:

and how ℂ and ℚ look different

You are describing a font issue. Probably the font you are using only has one of them.