mathlib documentation


Topology on filters of a space with order topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that 𝓝 (f x) tends to 𝓝 filter.at_top provided that f tends to filter.at_top, and similarly for filter.at_bot.