A net in a set is a directed set and a function ; we say that indexes the net. The notation used is based on the special case of an infinite sequence; the value of the function at the index is written . Indeed, an infinite sequence in is a net indexed by the natural numbers.
Although , being a directed set, is equipped with a preorder, the net is not required to preserve this in any way. This forms an exception to the rule of thumb that a preordered set may be replaced by its quotient poset. You can get around this if you instead define a net in as a multi-valued function from a partially ordered directed set to . Although there is not much point to doing this in general, it can make a difference if you put restrictions on the possibilities for , in particular if you consider the definition of sequence. In some type-theoretic foundations of mathematics, you can get the same effect by defining a net to be an ‘operation’ (a prefunction, like a function but not required to preserve equality).
There are several different definitions of ‘subnet’ in the literature, all of which intend to generalise subsequences. We give them in order of increasing generality. Note that it is Definition 3 which is correct in that it corresponds precisely to refinement of filters. However, the other two definitions are sufficient (in a sense to be made precise at the end of this section) and may be easier to work with.
Given a net with index set , and a net with an index set , we say that is a subnet of if:
We have a function such that
We have a function such that
(Smiley, 1957; Årnes & Andenæs, 1972).
The eventuality filter of (see below) refines the eventuality filter of . (Explicitly, for every there is a such that, for every there is an such that .)
The equivalence between these is as follows:
A property of elements of (given by a subset of ) can be applied to nets in .
We say that is eventually in if for some index , for every . Dually, we say that is frequently in if for every index , for some .
Sometimes one says ‘infinitely often’ in place of ‘frequently’ and even ‘cofinitely often’ in place of ‘eventually’; these derive from the special case of sequences, where they may be taken literally.
Being eventually in , def. 4, is a weakening of being always in (given by Lawvere's universal quantifier ), while being frequently in is a strengthening of being sometime in (given by the particular quantifier ). Indeed we can build a formal logic out of these. Use or to mean that a predicate in is eventually true, and use or to mean that is frequently true. Then we have:
A net in a set defines a proper filter of subsets of , called the eventuality filter of the net. It consists simply of those subsets of that is eventually in, def. 4. (Recall that a filter of subsets is a collection of subsets that is closed under intersection and taking supersets; the filter is proper if each set in it is inhabited.)
Conversely, any filter defines a net whose eventuality filter is . Let be the disjoint union of ; that is, an element of is of the form , where . Define iff (regardless of and ). Since is a filter, one can show that is a directed set (one needs here that is proper). Define to be ; then is a net in whose eventuality filter is again. (It is actually enough to use only a base of the filter when defining .)
Nets are considered equivalent if they have the same eventuality filter; in other words, they are both subnets of each other. In particular, they define the same logical quantifiers and are therefore equivalent for the application to topology below. (Of course, it is possible to distinguish them by using the standard logical quantifiers instead.)
A net in a topological space converges to a point in the space if, given any neighbourhood of , is eventually in (def. 4); clusters at if, for every neighbourhood of , is frequently in (also def. 4). One can in fact recover the topology on the set simply by knowing which nets converge to which points. It is possible to define elementary conditions on this convergence relation that characterise whether it is topological (that is whether it comes from a topology on ), although these are a bit complicated.
By keeping only the simple conditions, one gets the definition of a convergence space; this is a more general concept than a topological space and includes many non-topological situations where we want to say that a sequence converges to some value (such as convergence in measure). It is also very nice to describe compact and Hausdorff spaces in terms of the convergence relation.
Although nets are perhaps more familiar, due to their similarity to sequences, one gets a cleaner theory by talking about filters, since equivalent filters are equal and (as long as one is not a predicativist) the set of filters on a set is small (not a proper class).