Notation for ennreal

Stream: general

[Floris van Doorn]

I think mathlib should adopt notation for ennreal, which is hard to parse if you first see it. On paper I would write $[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.

[Patrick Massot]

I certainly agree ennreal is hard to read.

[Johan Commelin]

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

[Gabriel Ebner]

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.

[Floris van Doorn]

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}

[Gabriel Ebner]

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

[Floris van Doorn]

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..∞].

[Floris van Doorn]

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.

[Johan Commelin]

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.

[Eric Wieser]

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

[Sebastien Gouezel]

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)

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Floris van Doorn]

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

[Floris van Doorn]

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

[Rémy Degenne]

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?

[Gabriel Ebner]

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

[Gabriel Ebner]

PRs welcome.

[Rémy Degenne]

Thanks!