The theory described in this paper is a drop in the ocean of continuous lattices theory (see [CCL]). It is included in the theory of topologies defined on a lattice (poset) directly from the lattice (poset) ordering. Birkhoff and Frink started the investigations for symmetric lattices (see [B&F,Fr]). Scott began investigations of topologies of sets inaccessible by directed sets, or so called Scott topologies (for the Mizar formalization see [W11] and [W14]). In such cases, topologies induced by an order and its reverse are different. We may say that a Scott topology is a one-side topology (open sets are upper sets). It is an example of an order consisting topology (see [W32]). Lawson proposed to study the refinement of a Scott topology and a lower topology (see [CCL]). The refinement is still asymmetric but it is a compact Hausdorff topology in contrast to a Scott topology (see [CCL] or [W19]). The lim-inf topologies are topologies induced by convergence classes defined in terms of a lattice supremum and infimum. They are equivalent to Lawson topologies for meet-continuous lattices described in [W2]. Our partial goal is to prove the equivalence in Mizar. At this time, half of the proof, concerning compactness of lim-inf topology, is done.
The work presented in this paper is part of a bigger project - the formalization in Mizar of the theory of continuous lattices first described in [Ban]. It is an international project started in 1996 and is devoted to formalizing the theory from [CCL]. It was originally motivated by the question of whether the Mizar system is sufficiently developed for the expression of advanced mathematics. The current state of the formalization, which includes 57 Mizar articles written by 16 authors from Poland, Japan, and Canada, suggests that the answer is positive.
In this paper, we do not give strict definitions and precise proofs, but rather we intend to describe the general approach to formalization chosen by the authors of the Mizar articles in this work. For more details we ask the readers to see the Mizar articles listed in the references. Other aspects of the theory of continuous lattices may be found in the Mizar Mathematical Library (MML)2 in articles with identifiers starting with "WAYBEL".