Zulip Chat Archive
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 . 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 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
Gabriel Ebner (Feb 08 2021 at 13:54):
PRs welcome.
Rémy Degenne (Feb 08 2021 at 13:57):
Thanks!
Last updated: Dec 20 2023 at 11:08 UTC