A better notation for limit

[akp2003]

It is my first time opening an issue.
Here is the zulip topic

Is there a better notation for the limit in mathlib ?
like lim x → -∞ , (∫ (t : ℝ) in Iic x, f t) = 0 instead of Tendsto (fun x ↦ ∫ (t : ℝ) in Iic x, f t) atBot (𝓝 0)

It would be great if someone could add this notation to mathlib.

[vihdzp]

I understand making notation for this is quite difficult due to the sheer generality. But really I'd be satisfied with basically anything using lim or →; I think it'd do wonders for readability.