Zulip Chat Archive

Stream: general

Topic: Strong binding power


Patrick Massot (Oct 21 2019 at 13:38):

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 (Oct 21 2019 at 13:41):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC