nLab eventuality filter

Eventuality filters




topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory

Eventuality filters


Eventuality filters are the key translation between filters and nets in analysis and topology. Specifically:

  • Given a net nn (or in particular a sequence) in a set XX, the eventuality filter of nn is a proper filter on XX;

  • Every proper filter on XX is the eventuality filter of some net in XX;

  • Two nets are equivalent for purposes of convergence (meaning precisely that they are subnets of each other in the sense of Årnes & Andenæs) if and only if their eventuality filters are equal.

This last point is not so much a result as the definition of the subnet relation (or at least of its symmetrisation, the relation of equivalence of nets). One still needs to check that every use of nets in analysis and topology (or other fields) actually respects this notion of equivalence of nets, if one wishes to convert nets to filters.


Let XX be a set, let DD be a directed set, and let nn be a function from DD to XX, so that nn is a net in XX. Given a subset AA of XX, nn is eventually in AA if, for some ii in DD, for each jij \geq i in DD, n jAn_j \in A. The collection F nF_n of all those subsets AA such that nn is eventually in AA is a proper filter on XX, called the eventuality filter of nn.

In symbols,

F n{AX|essj,n jA}, F_n \coloneqq \{ A \subseteq X \;|\; \ess \forall\, j,\; n_j \in A \} ,

where essj\ess \forall\, j is read ‘for essentially each jj’ or ‘eventually for each jj’ and means i,ji\exists\, i,\; \forall j \geq i. In the case where DD is the set of natural numbers directed by \leq, so that nn is an infinite sequence (ω\omega-sequence) in XX, then essj\ess \forall\, j may be read as ‘for all but finitely many jj’.


Given a filter FF on XX, let DD be the binary relation X\in_X restricted to FF, viewed as a subset of the cartesian product X×FX \times F, ordered so that (y,A)(z,B)(y, A) \leq (z, B) means simply that BAB \subseteq A. Let n:DXn\colon D \to X map (y,A)(y, A) simply to yy. Then DD is directed (so that nn is a net in XX) iff FF is proper; and in that case, the eventuality filter of the net nn is FF.

It is possible to define DD as X| F×{{\in_X}|_F} \times \mathbb{N} (instead of as X| F{\in_X}|_F as done above) so that the direction on DD is a partial order, if one really wants to. (Then (y,A,i)(z,B,j)(y, A, i) \leq (z, B, j) means that BAB \subseteq A, iji \leq j, and y=zy = z if i=ji = j.)

Last revised on May 29, 2022 at 16:17:55. See the history of this page for a list of all contributions to it.