The Scott topology

One of the objectives of the theory of continuous lattices is a characterization of the correspondence between lattice theoretic notions and topological notions. The starting point for the algebraic side is the notion of lim-inf convergence formalized in WAYBEL11 [53] as

definition let R be non empty RelStr, N be net of R;
 func lim_inf N -> Element of R equals               :: WAYBEL11:def 6
 "\/" ( { "/\"( { N.i : i >= j }, R )
          where j is Element of the carrier of N: not contradiction 
        }, R );
end;

where "/\"(X,R) is the infimum and "\/"(X,R) is the supremum of X wrt R, respectively. Now, one is in a position to construct Scott's topology. First, we define the Scott convergence class

definition let R be reflexive non empty RelStr;
 func Scott-Convergence R 
                     -> Convergence-Class of R means :: WAYBEL11:def 8
 for N being strict net of R st N in NetUniv R
 for p being Element of the carrier of R
  holds [N, p] in it iff p <= lim_inf N;
end;

A TopRelStr is Scott according to definition WAYBEL11:def 4 quoted in Section  where open sets are characterized in lattice terms. One now proves the key theorem:

theorem                                                 :: WAYBEL11:32 
for T being complete Scott TopLattice
 holds the TopStruct of T = ConvergenceSpace Scott-Convergence T;

(cf. Section ). In addition, for every complete and continuous LATTICE, its Scott-Convergence is topological, i.e., it satisfies the conditions stated in Figure . In order to follow the CCL-book, we also defined a separate functor denoting the Scott topology

definition let L be non empty reflexive RelStr;
 func sigma L -> Subset-Family of L equals          :: WAYBEL11:def 12
 the topology of ConvergenceSpace Scott-Convergence L;
end;

The formalization of Scott's topology was finished in WAYBEL14 [21]. In the proof of

1.15. Corollary. For any complete lattice $L$ the following conditions are equivalent

(1)

$L$ is algebraic.

(2)

The Scott topology has a basis of sets $\uparrow\!k$ where $k \in K(L)$

(3)

$\sigma(L)$ is algebraic and has enough co-primes.

from [25, p. 108], a simplification was found. Typically, theorems of this form are proven as a sequence of implications, say $(1) \Rightarrow (2)$, $(2) \Rightarrow (3)$ and $(3) \Rightarrow (1)$, and this is indeed what is done in the CCL-book. While formalizing the last implication, we could not follow one of the given hints and thus we completed the proof by proving $(3) \Rightarrow (2)$ and then $(2) \Rightarrow (1)$. The proof in the book turned out to be correct, but we ended up with a simpler proof. A small reward for all these formalization chores!