The Lawson topology

The Lawson topology is formalized in WAYBEL19 [12] as a refinement of Scott's topology and the so called lower topology. The latter is defined as

definition :: 1.1. DEFINITION, p. 142 (part I)
 let T be non empty TopRelStr;
 attr T is lower means                               :: WAYBEL19:def 1
  { -uparrow x where x is Element of T: not contradiction } 
   is prebasis of T;
end;

The Lawson topology is then defined as

definition :: 1.5. DEFINITION, p. 144 (part I)
 let T be reflexive (non empty TopRelStr);
 attr T is Lawson means                              :: WAYBEL19:def 3
  (omega T) \/ (sigma T) is prebasis of T;
end;

where omega T is the lower topology and sigma T is the Scott topology. The formalization of the material on Lawson's topology has not been completed; of 55 items, 17 are still not done and the material in these remaining items becomes more and more advanced. Article WAYBEL21 [13] can serve as a case in point of the volume of preparatory material needed to prove the more advanced items.

Article WAYBEL21 formalizes two items from the CCL-book, Theorem 1.8 from p. 145 and Theorem 1.11 from pp. 146-147. Both theorems state the equivalence of three statements, thus their proofs consist of justifying sequences of implications. The entire article is 2,130 lines long and the actual proofs of theorems take only 400 lines. But 1600 lines were needed to develop some auxiliary, frequently very technical, facts such as: properties of semi-lattices and morphisms of SubRelStrs. These properties probably also have potential for reuse, but really belong to the YELLOW series. The remaining 100 lines concern a generalization of Lemma 1.7 from [25, p. 145]

1.7. LEMMA. Let $L$ be a complete lattice and $F$ a filtered subset. Then $\inf F = \lim F$ with respect to $\lambda(L)$, and this limit is unique.

($\lambda(L)$ is the Lawson topology for $L$). A formalization of this lemma, by the same author, originally appeared in WAYBEL19 [12] as

theorem                                                 :: WAYBEL19:43
 for T being Lawson (complete TopLattice),
      F being non empty filtered Subset of T
  holds Lim (F opp+id) = {inf F};

and then its revised version was put into WAYBEL21 [13]

theorem                                                 :: WAYBEL21:44 
                                 :: 1.7. LEMMA, -- WAYBEL19:43 revised
 for T being Lawson (complete TopLattice)
     N being eventually-filtered net of T
  holds Lim N = {inf N};

Without going into the details of both formulations of the lemma, we simply note that we frequently faced similar situations in which it was unclear whether we should keep one version of the theorem, or the other, or both. If we kept only one then would it be in the original article or the new one? Depending on the answer to this question, revisions of past work became necessary and tools automating the process of such revisions are being considered. The frequency of such cases prompted more discussion about a long pending redesign $^{\alph{endnotexboole}}$ of the organization of MML (see Section ).