Zulip Chat Archive

Stream: general

Topic: Strong binding power


view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 21 2019 at 13:41):

(deleted)


Last updated: May 14 2021 at 04:22 UTC