notation for positive elements

Stream: general

[Damiano Testa]

Dear All,

I am trying to find a good notation for the type of positive elements of a type with 0 and <. Below are some suggestions: I have tested them a little, but I am not sure that they will not cause other problems. Feel free to vote for one of the existing ones or to add choices!

Thanks!

variables (α : Type*) [has_zero α] [has_lt α]

@[reducible]
def pos := {x : α // 0 < x}

notation ??? := pos α

[Damiano Testa]

/poll Notation for positive elements
α›0
α>0
α>₀
α₊₀
α₊

[Floris van Doorn]

What is wrong with {x : α // 0 < x}? I was happy with the corresponding notation in file#algebra/order/nonneg.

[Alex J. Best]

I would say the downside is its quite long. That's a lot of characters to represent a fairly simple idea

[Damiano Testa]

I agree with Alex: it works, but is long and not as catchy as, for instance, ℝ≥0.

[Damiano Testa]

Although it is a possibility: I will add it to the list! (I did not know that the backticks do not work in polls.)

[Floris van Doorn]

If the >0 in option 2 consists of two ASCII characters, I would like to note that that option implies that you are never able to write _ > 0 without space anymore (and Lean will give a cryptic error message if you do).

[Yaël Dillies]

What I really want is α\_>₀, but Unicode is lacking...

[Damiano Testa]

Floris van Doorn said:

If the >0 in option 2 consists of two ASCII characters, I would like to note that that option implies that you are never able to write _ > 0 without space anymore (and Lean will give a cryptic error message if you do).

Ok, so, even though I forgot the meaning of the symbol >, thanks to mathlib, this is probably a good reason to remove this one from the list.

[Yaël Dillies]

What Unicode has to offer (search for GREATER)

[Shing Tak Lam]

Yaël Dillies said:

What Unicode has to offer (search for GREATER)

There's also https://unicode-table.com/en/1433/ (ᐳ)

("If you look closely, those aren't angle brackets, they're characters from the Canadian Aboriginal Syllabics block")

edit: also https://shapecatcher.com/ is good for finding things with the shape of a > but isn't >

[Damiano Testa]

Wow!! Thanks!

This means that this is also an option:

α˃⁰

[Damiano Testa]

(Added this choice above: it looks much better in the poll than here.)

[Vincent Beffara]

In the French tradition, $\mathbb R_+$ is $\{x \in \mathbb R, 0 \le x\}$ so $\alpha_+$ would be a little confusing as meaning the strict inequality

[Eric Rodriguez]

we have ℕ with zero, so sometimes these things have to be done

[Vincent Beffara]

Do there need to be a companion notation for le instead of lt?

[Reid Barton]

FWIW homotopy theorists also use ${X}_{+}$ to mean basically option X, and I assume this notation is also popular in other fields with other meanings (like $f_+ = \max \{f, 0\}$), so maybe better not to reserve a global meaning for it

[Reid Barton]

also in pretty much the next topic I clicked on I saw ⌊x⌋₊, which I don't know the meaning of but looks likely to conflict

[Yaël Dillies]

docs#nat.floor

[Yury G. Kudryashov]

I don't think that "ε>0 doesn't work" is really bad. I would say that "insert spaces around binary operations and relations, otherwise you may hit a notation" is not that bad.

[Yury G. Kudryashov]

Another option is to use

local notation `α>0` := {x : α // 0 < x}

(one line per relevant type variable) in files that deal with general theory and register, e.g., ℝ>0, ℚ>0 globally.

[Yaël Dillies]

I've added a bunch of spaces around notation myself, so i'm all in favor of enforcing it more.

[Reid Barton]

Yury G. Kudryashov said:

I don't think that "ε>0 doesn't work" is really bad. I would say that "insert spaces around binary operations and relations, otherwise you may hit a notation" is not that bad.

One downside is that maybe "we" all know that you need to put spaces in ε > 0, but a new user might write ∀ε>0 and get a totally baffling error message (I'm assuming).

[Eric Wieser]

if we put it in a locale, then such a user would have had to opt in first

[Eric Wieser]

It would be nice if we could attach docstrings to locales so that hovering over open_locale foo gave some information about what the effect it

[Yaël Dillies]

That's actually a great idea!

[Damiano Testa]

I'm tempted to go with Yuri's suggestion of local notation with the α embedded into the symbol.

I think that for this PR it is easier like this. Changing it in a subsequent one will be easy, if desired!

[Damiano Testa]

I've also just found this:

α˲₀

I think that I'm going to use this, with α hardcoded in the notation, as per Yuri's suggestion!

[Eric Wieser]

I think using regular >0 would be better to match ℝ≥0

[Eric Wieser]

Unless we change both

[Damiano Testa]

Fair enough: I like the consistency argument!