InitialSeg notation3

Stream: mathlib4

[Eric Paul]

The ≤i notation for InitialSeg is defined as follows

notation:25 α:24 " ≤i " β:25 => @InitialSeg α β (· < ·) (· < ·)

in docs#«term_≤i_»

This means that in the infoview the notation is not shown. I was hoping this could be changed to show the notation in the infoview. For example, switching to notation3 fixes this. Is this a reasonable change?

[Eric Paul]

I realize now that doing open InitialSeg makes this correctly be an abbreviation for the ≼i notation. I however would still prefer if it was not an abbreviation for the other notation but notation in its own right since I'm always thinking about one linear order being an initial segment of another.

[Kyle Miller]

I think it's ok changing notation to notation3 if it helps with pretty printing. I hope eventually notation can do it itself.

[Eric Paul]

My main hesitation in making such a change is that the documentation at the top of page states
"α ≤i β is an abbreviation for (· < ·) ≼i (· < ·)" which makes me wonder if it was chosen to be an abbreviation for a certain reason.