Filter.atTop in specific direction

Stream: Is there code for X?

[Peter Pfaffelhuber]

When learning mathlib, I learned about filters. I wonder why I cannot find a version of the atTop-filter, which goes to ⊤ only in a specific direction. What I mean is:

def atTopOf [LE α] (p : α → Prop) : Filter α :=
  ⨅ x ∈ {y | p y}, 𝓟 {b | x ≤ b}

For example, this filter can be used to formulate tight families of measures (already in Mathlib, using a different definition), but I am sure there are lots of other examples where one wants to restrict convergence into a certain direction.

def IsTightMeasureSet (S : Set (Measure α)) := Tendsto (fun A ↦ ⨆ ℙ ∈ S, ℙ Aᶜ) (atTopOf IsCompact) (nhds 0)

[Pontus Sundqvist]

Maybe docs#nhdsWithin would be useful

[Floris van Doorn]

I could imagine that this atTopOf (or atTopAbove, atTopIn?) filter could be useful, and if you have a use case where it significantly simplifies an argument, I'm sure that Mathlib would be happy to include it.