Filter limit

Remarks

Equivalently, the image filter $f(\mathcal{F}) = \set{B \subseteq X : f^{-1}(B) \in \mathcal{F}}$ converges to $x$.

Example: on $S = \N$ let $\mathcal{F}$ be the filter of sets that contain $\set{n : n \ge N}$ for some $N$; in Mathlib this is Filter.atTop. A sequence $f(n) = x_n$ tends to $x$ along $\mathcal{F}$ exactly when for every neighbourhood $U$ of $x$ there is $N$ with $x_n \in U$ for all $n \ge N$. This is the usual convergence of a sequence.

Non-example: the sequence $f(n) = (-1)^n$ in $\R$ has no limit along this filter. For $x \ne 1$, some neighbourhood of $x$ misses $1$, so its preimage misses all even numbers and contains no tail. For $x = 1$, the preimage of $(0, 2)$ is the set of even numbers, which contains no tail either.

Example: for $a \in \R$, the sets $V \setminus \set{a}$ with $V$ a neighbourhood of $a$ generate a filter on $\R \setminus \set{a}$, and the limit along it is the usual limit $\lim_{t \to a} f(t)$.

If $X$ is Hausdorff and $\emptyset \notin \mathcal{F}$, then $f$ has at most one limit along $\mathcal{F}$.