limit notation

Stream: maths

[Patrick Massot]

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

[Patrick Massot]

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.

[Johan Commelin]

I don't really have an opinion.

[Johan Commelin]

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

[Johan Commelin]

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