scoped notation I

Stream: mathlib4

[Johan Commelin]

--- Porting note: removed `scoped[uIcc]` temporarily before a workaround is found
 -- Below is a capital iota
 /-- `Ι a b` denotes the open-closed interval with unordered bounds. Here, `Ι` is a capital iota,
 distinguished from a capital `i`. -/
-notation "Ι" => Set.uIoc
+scoped[uIcc] notation "Ι" => Set.uIoc
+
+open scoped uIcc

causes a cascade of fixes to Mathlib, of which I haven't yet seen the end. See https://github.com/leanprover-community/mathlib4/compare/917b269...jmc-uicc?expand=1
Is this what we want? Or should we scope this in Interval? Or just leave it as is?

[Johan Commelin]

/poll What shall we do with the I notation for the unit interval?

• Status quo: global notation
• Scope in Interval
• Scope in uIcc (see diff above)

[Kevin Buzzard]

uIoc scoped in uIcc?

[Patrick Massot]

I am very strongly against the global notation option. Very generic global notation for specialized notions are really a pain. I’ve been hit by this many times.

[Johan Commelin]

Lol, I only looked at the porting note...

[Johan Commelin]

Returning to this again. I'll go with the Interval scope.

[Johan Commelin]

chore: scope Interval notation #24433

[Yury G. Kudryashov]

I would drop this notation.

[Yury G. Kudryashov]

It doesn't save key strokes and IMHO it's less readable than uIoc.