## Stream: new members

### Topic: limit on one side

#### Anatole Dedecker (Jun 23 2020 at 20:56):

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 (Jun 23 2020 at 21:18):

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

#### Patrick Massot (Jun 23 2020 at 21:20):

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

#### Anatole Dedecker (Jun 23 2020 at 21:28):

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

Last updated: May 14 2021 at 07:19 UTC