Moore-Smith convergence

The CCL-book uses Moore-Smith convergence classes to justify that the Scott topology is adequate for describing the required lim-inf convergence (see Section ) in topological terms. This posed quite a challenge for formalization in YELLOW_6 [52] as [25, pp. 101-102] makes only a reference to [32] and A. Trybulec ended up constructing convergence classes in MIZAR from scratch.

In Moore-Smith convergence theory, the concept of a net is a generalization of the concept of a sequence; nets are sometimes called generalized sequences. A sequence is a function on $\omega$ (linearly ordered by inclusion) and its generalization consists in a weakening of the ordering conditions on the index set, that is, the sequence domain. Nets are formalized in WAYBEL_0 [6] based on a new structure NetStr over S which is derived from the relational structure RelStr by augmenting it with a mapping from the indices--the carrier of the RelStr--into the carrier of the 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;

The carrier of S is the set on which we want to discuss a topology. Note that the carrier of S is not a field in NetStr as S is a parameter and not a structural ancestor of NetStr.

For a NetStr over S to be a net on the carrier of S it must be non empty, the indices must be directed, and the order must be transitive. This is expressed by two expandable type definitions in WAYBEL_0 [6]

definition let L be 1-sorted;
 mode prenet of L is directed non empty NetStr over L;
end;

definition let L be 1-sorted;
 mode net of L is transitive prenet of L;
end;

``Usual'' sequences satisfy all these conditions as $\omega$ is non empty and linearly ordered by inclusion. Thus, $\omega$ is a directed set.

We present below the convergence of nets based on [32]. Consider a net of L, N. We say that net N is eventually in X if there is an upper cone of indices with values of N in X. This is captured by the MIZAR predicate

definition 
 let L be non empty 1-sorted, N be non empty NetStr over L, X be set;
 pred N is_eventually_in X means                    :: WAYBEL_0:def 11
  ex i being Element of N st
   for j being Element of N st i <= j holds N.j in X;
end;

Given a topological space T, a net of T is said to be convergent to a point p of T iff it is eventually in every neighborhood of x. Since in general a net may converge to more than one point, a functor for denoting the set of all limits of a net is introduced.

definition let T be non empty TopSpace, N be net of T;
 func Lim N -> Subset of T means                    :: YELLOW_6:def 18
 for p being Point of T holds p in it iff
  for V being a_neighborhood of p holds N is_eventually_in V;
end;

We say that a net N is convergent if Lim N is non empty. Now, we may express the Moore-Smith concept of a convergence class where the key question is (cf. [32, p. 73]):

If $\mathcal{C}$ is a class consisting of pairs $(S,s)$, where $S$ is a net in $X$ and $s$ is a point, when there is a topology $\mathcal{T}$ for $X$ such that $(S,s) \in \mathcal{C}$ iff $S$ converges to $s$ relative to the topology $\mathcal{T}$?

Figure 1: Topological convergence conditions

The conditions that $\mathcal{C}$ must satisfy for such a topology to exist are stated in [32, p. 74] (recast informally in Figure ) and every class satisfying these conditions is called a convergence class. Our problem here is simple: in order to discuss convergence classes what should the domain(s) of these nets be? There are no classes in MIZAR and thus we could not follow the approach from [32]. The problem is in finding a set big enough to serve as the domain of our nets such that for any $\mathcal{C}$ and $\mathcal{T}$, we have $\mathcal{C}$ induces $\mathcal{T}$ iff $\mathcal{T}$ induces $\mathcal{C}$.

Fortunately, the Tarski-Grothendieck set theory available in MML allows for the construction of universal sets. In our case, the smallest universal class of a set is sufficiently large. More specifically, the following mode is used for convergence classes of the carrier of S (see YELLOW_6 [52] for details)

definition let S be non empty 1-sorted;
 mode Convergence-Class of S means                  :: YELLOW_6:def 21
  it c= [: NetUniv S, the carrier of S :];
end;

where

definition let X be non empty 1-sorted;
 func NetUniv X means                               :: YELLOW_6:def 14
 for x holds x in it iff
   ex N being strict net of X st N = x &
    the carrier of N in the_universe_of the carrier of X;
end;

and the_universe_of a set A is a set B having the $\epsilon$-transitive closure of A as an element and satisfying the following conditions defined in CLASSES1 [1].

definition let B be set;
 attr B is being_Tarski-Class means                  :: CLASSES1:def 2
  B is subset-closed &
  (for X being set holds X in B implies bool X in B) &
  (for X holds X c= B implies X, B are_equipotent or X in B);
end;

Given a convergence class we can form a topological space as follows

definition let S be non empty 1-sorted, C be Convergence-Class of S;
 func ConvergenceSpace C -> strict TopStruct means  :: YELLOW_6:def 27
 the carrier of it = the carrier of S &
 the topology of it = 
  { V where V is Subset of the carrier of S:
    for p being Element of the carrier of S st p in V
     for N being net of S st [N, p] in C holds N is_eventually_in V };
end;

A convergence class is called topological if it satisfies the conditions stated in Figure . The key theorems then state that

theorem                                                 :: YELLOW_6:49 
for S be non empty 1-sorted, C be Convergence-Class of S
 holds C c= Convergence ConvergenceSpace C;

theorem                                                 :: YELLOW_6:53
for T be non empty 1-sorted, C be Convergence-Class of T
 holds Convergence ConvergenceSpace C = C iff C is topological;

The point that we would like to make here is this: fortunately for our project, MML contained the theory of Tarski universal classes as without it, the detour in formalizing the notion of a convergence class and thus Scott's topology (see Section ) would have been much longer.