Do mathlib have at_top_bot filter

Stream: Is there code for X?

[Meow]

Do mathlib have a filter at_top_bot defined as the supermum of at_top and at_bot? If we have it, we can easily define exp_decay as =O[at_top_bot] exp (-b*|x|).

[Junyan Xu]

You probably want docs#filter.cocompact; docs#zero_at_infty_continuous_map is defined in terms of it.

[David Loeffler]

Some little bit of checking is required to show that the cocompact filter on R is the supremum of at_top and at_bot, I guess.