Zulip Chat Archive

Stream: maths

Topic: limit notation


view this post on Zulip Patrick Massot (Aug 25 2020 at 16:35):

Should we get rid of notation f `→_{`:50 a `}`:0 b := filter.tendsto f (_root_.nhds a) (_root_.nhds b)? I wrote that line after using Lean for about one month I think, at a time when I was still afraid of filters. Now I find it distracting (and slightly embarrassing).

view this post on Zulip Patrick Massot (Aug 25 2020 at 16:36):

What makes things worse than having notation only for this special case is it's defined in normed_space.basic so it will show up only in files importing that one.

view this post on Zulip Johan Commelin (Aug 26 2020 at 06:26):

I don't really have an opinion.

view this post on Zulip Johan Commelin (Aug 26 2020 at 06:27):

We do want to avoid a too high barrier of entry for old-skool mathematicians that don't know what a filter is.

view this post on Zulip Johan Commelin (Aug 26 2020 at 06:28):

But I guess this notation doesn't necessarily help with that.


Last updated: May 11 2021 at 16:22 UTC