mathlib documentation

topology.algebra.order.filter

Topology on filters of a space with order topology #

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.