Zulip Chat Archive

Stream: general

Topic: Notation for ennreal


view this post on Zulip Floris van Doorn (Feb 02 2021 at 20:02):

I think mathlib should adopt notation for ennreal, which is hard to parse if you first see it. On paper I would write [0,][0,\infty]. You cannot define custom notation with , so I suggest the notation [0..∞].

I started this on branch#ennreal-notation, but I wanted to check if there are any objections before changing it everywhere.

view this post on Zulip Patrick Massot (Feb 02 2021 at 20:04):

I certainly agree ennreal is hard to read.

view this post on Zulip Johan Commelin (Feb 02 2021 at 20:06):

I think your suggestion is fine. It's pretty self-explanatory.

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 20:07):

My first thought when seeing this notation is that it means Icc 0 ∞. I would have expected ℝ⁺∞ or ℝ≥0∞ for the type. But that's just my first impression.

view this post on Zulip Floris van Doorn (Feb 02 2021 at 20:10):

There is a similar question for the intervals Ixx. This is a bit trickier, since we cannot use parentheses in notation. We could do something similar to Isabelle, which uses {..<u}, {l..}, and {l<..u} for Iio u, Ici l and Ioc l u.
We could use as well: {..<u}, {l≤..}, and {l<..≤u}

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 20:12):

I don't think this works in Lean 3, {..u} is already taken, and we can't realistically override {.

view this post on Zulip Floris van Doorn (Feb 02 2021 at 20:12):

Gabriel Ebner said:

My first thought when seeing this notation is that it means Icc 0 ∞. I would have expected ℝ⁺∞ or ℝ≥0∞ for the type. But that's just my first impression.

@Gabriel Ebner something like that is possible too, but I prefer [0..∞].

view this post on Zulip Floris van Doorn (Feb 02 2021 at 20:13):

Oh, good point. Maybe with square brackets? Though that might also conflict with other notation and I'm not sure if that is more readable then.

view this post on Zulip Johan Commelin (Feb 02 2021 at 20:14):

Gabriel Ebner said:

My first thought when seeing this notation is that it means Icc 0 ∞. I would have expected ℝ⁺∞ or ℝ≥0∞ for the type. But that's just my first impression.

Hmm, I like ℝ≥0∞ as well... it's more in line with the notation for nnreal.

view this post on Zulip Eric Wieser (Feb 02 2021 at 20:33):

As types, are Icc 0 (info : ereal) and ennreal isomorphic?

view this post on Zulip Sebastien Gouezel (Feb 02 2021 at 20:34):

At least, the .. is not a real issue, you can use any unicode variant like (I just typed \ldots in vscode, and it gave me this)

view this post on Zulip Sebastien Gouezel (Feb 02 2021 at 20:36):

And you can use fancy brackets like for the end of the interval.

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 20:59):

Out of interest, will we be able to do [0,][0,\infty] in Lean 4?

view this post on Zulip Kevin Buzzard (Feb 02 2021 at 21:00):

PS I am also very happy with the [0..\infty] idea.

view this post on Zulip Floris van Doorn (Feb 02 2021 at 21:12):

/poll What should the notation for ennreal be?
[0..∞]
ℝ≥0∞

view this post on Zulip Floris van Doorn (Feb 04 2021 at 19:27):

I used ℝ≥0∞ following the majority in #6044

view this post on Zulip Rémy Degenne (Feb 08 2021 at 13:47):

I would like to define a shortcut for the ennreal notation, such that typing \ennreal writes ℝ≥0∞, like what we already have for nnreal, for which typing \nnreal produces ℝ≥0. However I don't know where those things are defined. Can someone help me do that?

view this post on Zulip Gabriel Ebner (Feb 08 2021 at 13:54):

https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json

view this post on Zulip Gabriel Ebner (Feb 08 2021 at 13:54):

PRs welcome.

view this post on Zulip Rémy Degenne (Feb 08 2021 at 13:57):

Thanks!


Last updated: May 13 2021 at 06:15 UTC