Nets and Moore-Smith convergence

The concept of nets is a generalization of the concept of topological sequences and sometimes nets are called generalized sequences. The generalization consists in the weakening of the ordering conditions of sequence indices. Nets are introduced in [W0] in this way as structural augmentations of relational structures (RelStr): the relation describes the order of indices (the carrier) and an additional field maps the indices into the carrier of the given structure $S$.

   definition
     let S be 1-sorted;
     struct(RelStr) NetStr over S (#
       carrier -> set,
       InternalRel -> Relation of the carrier,
       mapping -> Function of the carrier, the carrier of S
     #);
   end;

For a net structure over $S$ to be a net on $S$ it must be non empty, the indices must be directed, and the order must be transitive. In ``traditional'' sequences the order is linear, so indices are directed.

We say that a net is eventually in a set $X$ if for any index $i$ there exists a larger index $j$ such that all values of the net for indices larger than $j$ belong to the set $X$.

     for i ex j st j >= i & for k st k >= j holds N.k in X

In other words, arbitrarily large indices determine an upper cone of indices with values in the set $X$. In the case of traditional (linear) sequences, it means that almost all elements of the sequence belong to the set. A net is convergent to a point $x$ if and only if it is eventually in every neighborhood of $x$ (see [Y6]). This corresponds to the convergence of a sequence to $x$, which means that almost all elements of the sequence are in every neighborhood of $x$.

Now, we may formalize Moore and Smith's idea of a convergence class. We treat it as a set³of ordered pairs in which the first element is a net and the second is a convergence point of the net. For a given topological space $T$ we want to take a sufficiently large number of convergent nets on $T$ and their convergence points. To realize such an approach, we limit the family of all possible sets of indices to NetUniv $T$, the smallest universal set of the carrier of $T$ (see [Y6]). Due to the properties of convergence classes:

• for any topological space, the convergence class of it induces the same topology, and
• for any topological convergence class, the topology induced by it has the same class of convergence

this limitation turned out to be sufficient.