## Stream: general

### Topic: Notation for ennreal

#### 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,\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 (Feb 02 2021 at 20:04):

I certainly agree ennreal is hard to read.

#### Johan Commelin (Feb 02 2021 at 20:06):

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

#### 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.

#### 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}

#### 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 {.

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

#### 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.

#### 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.

#### Eric Wieser (Feb 02 2021 at 20:33):

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

#### 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)

#### Sebastien Gouezel (Feb 02 2021 at 20:36):

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

#### Kevin Buzzard (Feb 02 2021 at 20:59):

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

#### Kevin Buzzard (Feb 02 2021 at 21:00):

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

#### Floris van Doorn (Feb 02 2021 at 21:12):

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

#### Floris van Doorn (Feb 04 2021 at 19:27):

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

#### 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?

#### Gabriel Ebner (Feb 08 2021 at 13:54):

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

PRs welcome.

#### Rémy Degenne (Feb 08 2021 at 13:57):

Thanks!

Last updated: May 13 2021 at 06:15 UTC