Zulip Chat Archive

Stream: new members

Topic: limit on one side


view this post on Zulip 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...

view this post on Zulip Patrick Massot (Jun 23 2020 at 21:18):

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

view this post on Zulip Patrick Massot (Jun 23 2020 at 21:20):

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

view this post on Zulip 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