New segment notation

Stream: general

[Yaël Dillies]

I'm redefining everything in analysis.convex.basic to take in k, the underlying ordered_semiring, as an argument (it's currently always ℝ). So the notation [x, y] for segment x y needs changing to mention k.

What do you think of [x -[k] y]? This has also the advantage to make sure Lean isn't confused with list notation.

[Johan Commelin]

I think I could learn to like it (-;

[Yaël Dillies]

Would you even go to the extent of liking ]x -[k] y[ for open_segment k x y? :innocent:

[Johan Commelin]

I personally have never liked the inverted brackets notation. And I'm sure that syntax highlighters will also start crying (-;

[Oliver Nash]

Speaking only for myself, ]x -[k] y[ is a stretch too far.

[Eric Wieser]

How about [x, y][k]?

[Oliver Nash]

Or even [x,y:k] (if that's possible) or [x,y;k] etc?

[Eric Wieser]

Also you can likely keep the notation as [x, y] for places where k can be inferred

[Eric Wieser]

Maybe k ⬝ [x, y] to resemble the singleton span notation?

[Yaël Dillies]

Oliver Nash said:

Or even [x,y:k] (if that's possible) or [x,y;k] etc?

That's probably very bad considering type annotations.

[Oliver Nash]

Even with the semicolon?

[Yaël Dillies]

No, with the semicolon it should be fine.

[Oliver Nash]

Eric Wieser said:

Maybe k ⬝ [x, y] to resemble the singleton span notation?

This could be the best option but it slightly bothers me that this notation sort-of suggests [x, y] has a meaning on its own.

[Yaël Dillies]

My notation tries to look like the betweenness operator [a - b - c]

[Johan Commelin]

I think I like [x,y;k]. It's concise, which is good.

[Yaël Dillies]

Yaël Dillies said:

My notation tries to look like the betweenness operator [a - b - c]

and also like the linear_map and continuous_linear_map notation E →ₗ[k] F and E →L[k] F

[Patrick Massot]

Yaël, are you resurrecting #4787? In any case I wouldn't recognize any of the proposed notations, and I really hope the plain $[x, y]$ notation will be kept for the real case.

[Yaël Dillies]

Yes, but that's not what this PR is doing. #4787 generalizes to arbitrary affine spaces. I'm first generalizing to arbitrary vector spaces, then I will have a follow-up PR to generalize to affine spaces.

[Yaël Dillies]

$[x, y]$ notation is local anyway. So you can define it when needed for the real case, sure.