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):


Last updated: Aug 03 2023 at 10:10 UTC