limit on one side

Stream: new members

[Anatole Dedecker]

Hello, I can't find how to express the notion of \lim_{x\to a^+} in Lean, where a : real, do you know how to do it ? Again, I'm not sure which file to search in...

[Patrick Massot]

You need to search for nhds_within in topology/algebra/ordered

[Patrick Massot]

The filter corresponding to limit at $a^+$ is nhds_within a (Ioi a)

[Anatole Dedecker]

You didn't even let me the time to search :sob: But thanks !