filter tendsto limit from left right top bottom

Stream: Is there code for X?

[rtertr (Sonia)]

Hello! (Sorry for the bad title, just wanted the post to be found by the most people who could need it)

I want to use tendsto_nhds_unique: tendsto f l (nhds a) → tendsto f l (nhds b) → a = b where the filter l should be x -> 0+.
I haven't been able to find any lemmas about taking the limit from above/below. Is there any tendsto theorems like that somewhere? :)

Kind regards,

[Patrick Massot]

You should look at the list of variations on neighborhood filters at https://leanprover-community.github.io/mathlib_docs/topology/basic.html#notation

[Patrick Massot]

The one you want is 𝓝[>] 0.

[Patrick Massot]

import topology.instances.real

open filter
open_locale topology

example {X : Type*} [topological_space X] [t2_space X] {f : ℝ → X} {a b}
  (ha : tendsto f (𝓝[>] 0) (𝓝 a)) (hb : tendsto f (𝓝[>] 0) (𝓝 b)) : a = b :=
tendsto_nhds_unique ha hb

[rtertr (Sonia)]

Ah, great! Thank you :D