Strong binding power

Stream: general

[Patrick Massot]

Everywhere in the perfectoid project, I use

notation `𝓝` x:70 := nhds x

and I'd like to push this to mathlib, as a localized notation. In think the only controversial point is that 70. Is is bad? It makes possible to omit parentheses around 𝓝 x in a number of cases.

[Patrick Massot]

(deleted)