Recall that a *filter* on a set $X$ is a nonempty collection $\mathcal{F}$ of subsets of $X$ such that

(i) $U\subseteq V\subseteq X$ and $U\in\mathcal{F}$ implies $V\in\mathcal{F}$, and

(ii) $U,V\in\mathcal{F}$ implies $U\cap V\in\mathcal{F}$.

As far as I know, this definition was introduced by Bourbaki in "Topologie Generale", chapter 1 section 6 (the section is called "Filtres", and they furthermore demand that $\mathcal{F}$ does not contain the empty set, which I think nowadays some authors allow and some do not).

I'm giving a talk about filters to some 1st year undergraduates tomorrow, explaining how several distinct notions they've learnt in their course on sequences, series and continuity this term are special cases of the concept of a filter tending to a filter along a map. Let me explain this simple concept first, and then give examples of how it's used in the course.

If $\mathcal{F}$ is a filter on $X$ and $\mathcal{G}$ is a filter on $Y$, and $\phi:X\to Y$ is a map, then let's write $\mathcal{F}\rightarrow^\phi\mathcal{G}$ if for all $U\in\mathcal{G}$, we have $\phi^{-1}(U)\in\mathcal{F}$.

Examples:

1) if $C$ is the cofinite filter on $\mathbb{N}$ consisting of all sets with finite complement, if $\ell\in\mathbb{R}$ and $N(\ell)$ is the neighbourhood filter on $\mathbb{R}$, consisting of all sets whose interior contains $\ell$, and if $a:\mathbb{N}\to\mathbb{R}$ is a sequence, then the limit as $n\to\infty$ of $a(n)$ is $\ell$ iff $C\to^aN(\ell)$.

2) If $C$ is as above, and $N(\infty)$ is the filter on $\mathbb{R}$ is the filter of subsets containing $[B,\infty)$ for some $B\in\mathbb{R}$, then $a(n)\to\infty$ iff $C\to^aN(\infty)$.

3) If $f:\mathbb{R}\to\mathbb{R}$ then $N(x)\to^fN(f(x))$ iff $f$ is continuous at $x$.

So there's a proof that this is clearly a useful and standard idea. Ok now here's the stupid thing. I made up that notation $\mathcal{F}\to^\phi\mathcal{G}$ just now, because I actually learnt about this concept from the maths library of the Lean theorem prover , where it is called `tendsto φ ℱ 𝒢`

. This is very computer-sciency notation, so I went to the maths literature to find out what Bourbaki call this notion -- and I couldn't find it in there. Bourbaki talk about a filter tending to a limit on a topologcal space but this is a more specialised notion. I looked at some more topology books and couldn't find it there either. So then I asked the computer scientists who wrote this part of the maths library where it came from, and they told me that basically they made it up themselves, and they presumed it was in the maths literature but they didn't know where. They wanted to make pairs $(X,\mathcal{F})$ the objects of a category, and this is what they came up with for the morphisms.

The earliest reference I have to the concept is the definition from the Isabelle theorem prover, written by Johannes Hoelzl in November 2012.

This is surely a standard notion in the mathematical literature, but I can't find it. Where is it, and what is the notation we use for it?