Equivalence of two convergences

The other approach to convergence is filter convergence. Filters are introduced for relational structures as non empty, upper, and filtered subsets (see [W0]). We need filters on a set $X$, i.e., filters of $2^X_\subseteq$, the Boolean poset of the set $X$ (see [Y1]). In other words, filters on a set $X$ are non empty families of subsets of $X$ characterized by two conditions (see [W7]):

• closeness on supersets
• closeness on intersections.

The filter on a topological space is convergent to a point if every neighborhood of the point belongs to the filter.

An easy example of a filter on a topological space is the neighborhood system of a given point. Indeed, a superset of a neighborhood is itself a neighborhood and the intersection of two neighborhoods is also a neighborhood. The neighborhood system of a point $x$ is convergent to $x$.

Another example of a filter is the filter of a given net on $S$. It is a family of all subsets $A$ of $S$ such that the given net is eventually in $A$. Closeness on supersets is a direct consequence of the definition of the concept ``eventually in''. For the proof of closeness on the operation of intersection we must also apply the fact that indices form a directed set. The filter of a net convergent to a point $x$ is also convergent to $x$. This is one aspect of equivalence of two convergences.

The opposite conversion - from filters to nets - is more difficult. The net of a given filter is defined in [Y19] as follows:

   definition
     let S be non empty 1-sorted;
     let O be non empty Subset of S;
     let F be Filter of BoolePoset O;
     func a_net F -> strict non empty NetStr over S means
      the carrier of it = {[a, f] where a is Element of S,
                                    f is Element of F: a in f} &
      (for i,j being Element of it holds i <= j iff j`2 c= i`2) &
      for i being Element of it holds it.i = i`1;
   end;

For a proper filter $F$, the filter of the net of $F$ is equal to $F$. Finally, if a proper filter is convergent to a point $x$, then the net of it is also convergent to $x$.

This completes the expression of the equivalence of two convergences as it is worked out in [Y19].