Continuous lattices

The concept of a directed set was changed slightly in the MIZAR formalization. A directed set is non empty in math-lore and in the CCL-book. However, it happens frequently that we need a set which is directed or empty. MIZAR does not allow for the definition of a directed or empty set type and we decided to formalize the concept as follows

definition :: CCL, Definition 1.1, p. 2
  let L be RelStr, X be Subset of L;
  attr X is directed means                           :: WAYBEL_0:def 1     
   for x,y being Element of L st x in X & y in X
      ex z being Element of L st z in X & x <= z & y <= z;
end;

The theorem explaining correspondence to the usual meaning appears as

theorem                                                  :: WAYBEL_0:1
for L being non empty transitive RelStr, X being Subset of L 
 holds X is non empty directed 
   iff for Y being finite Subset of X
        ex x being Element of L st x in X & x is_>=_than Y;

The concept of completeness presented in the CCL-book depends on context. A complete poset, a complete semi-lattice, and a complete lattice have to satisfy different conditions. In MIZAR, we introduced the following attributes:

• up-complete for completeness with respect to directed sups,
• /\-complete for completeness with respect to non empty infs,
• complete for completeness with respect to all sups.

Then, we have the following correspondence

The CCL-book	MML
complete poset	up-complete Poset
complete semilattice	/\-complete up-complete Semilattice
complete lattice	complete LATTICE.

The fact that a complete lattice is both a complete poset and a complete semilattice is expressed in WAYBEL_0 [6] by the conditional cluster $\mathrm{registration}^{\:\alph{registrations}}$

definition
  cluster complete -> up-complete /\-complete 
                                        (non empty reflexive RelStr);
end;

The up-complete and /\-complete attributes are automatically added to an object already attributed by complete when its type widens to a non empty reflexive RelStr.

Since the concept of a continuous structure differs for lattices, semilattices, and posets in the CCL-book, we decided to formalize it in as general a way as possible by capturing the common meaning in the basic continuous attribute (see WAYBEL_3 [7]).

definition 
  let L be non empty reflexive RelStr;
  attr L is continuous means                         :: WAYBEL_3:def 6
   (for x being Element of L holds waybelow x is non empty directed) &
   L is up-complete satisfying_axiom_of_approximation;
end;

Note that our definition of continuity corresponds to Definition 1.26, p. 52 rather than Definition 1.6, p. 42 from the CCL-book. The attribute concerning the axiom of approximation is introduced as follows.

definition
  let L be non empty reflexive RelStr;
  attr L is satisfying_axiom_of_approximation means  :: WAYBEL_3:def 5
    for x being Element of L holds x = sup waybelow x;
end;

The sup functor is a supremum operator defined in YELLOW_0 [5]. The waybelow x is a set of all elements of L which are way below x as introduced by the following definitions in WAYBEL_3 [7]

definition  :: CCL 1.1, p. 38
 let L be non empty reflexive RelStr, x,y be Element of L;
 pred x is_way_below y means                         :: WAYBEL_3:def 1
  for D being non empty directed Subset of L st y <= sup D
   ex d being Element of L st d in D & x <= d;
 synonym x << y; synonym y >> x;
end;

definition  :: after CCL 1.2, p. 39
 let L be non empty reflexive RelStr, x be Element of L;
 func waybelow x -> Subset of L equals               :: WAYBEL_3:def 3
      {y where y is Element of L: y << x};
 func wayabove x -> Subset of L equals               :: WAYBEL_3:def 4
      {y where y is Element of L: y >> x};
end;

Our final notation for continuous structures is summarized below.

CCL	MML
continuous poset	continuous up-complete Poset
continuous semilattice	continuous up-complete Semilattice
complete-continuous	continuous /\-complete
semilattice	up-complete Semilattice
continuous lattice	continuous complete lattice

As a test of the correctness of the introduced concepts, we proved the correspondence between locally compact topological spaces and continuous lattices (see CCL [25,  p. 42]). This correspondence is expressed by two theorems

theorem                                                 :: WAYBEL_3:42
 for T being non empty TopSpace
     st T is_T3 & InclPoset(the topology of T) is continuous
  holds T is locally-compact;
      
theorem                                                 :: WAYBEL_3:43
 for T being non empty TopSpace st T is locally-compact
  holds InclPoset(the topology of T) is continuous;

The InclPoset(the topology of T) is the poset of open sets of T with set inclusion as the InternalRel.

The entire CCL-book is written very carefully and it is hard to find errors Some errors found in CCL:

• In Chapter I, Remark 3.18, p. 73, in order to prove that (1) iff (3), one also needs $\mathcal{F}$ to be proper unless prime filters are proper which is not assumed in their definition.
• In Chapter I, Proposition 3.24, p. 75, it is not true that (2) implies (3), a counterexample is provided in WAYBEL_7 [9] theorem WAYBEL_7:41.

of substance. Sometimes, however, we found theorems whose proofs as suggested in the CCL-book seemed too tedious to formalize and we ended up with different proofs. A case in point is the following

2.7. Theorem. The class of continuous lattices is closed under the formation of arbitrary products ...

(i)

If $L_j :j \in J$ is a family of continuous lattices, then the cartesian product ${\mathbf X}_{j \in J} L_j$ is a continuous lattice (relative to the component-wise partial order);

from [25, p. 60] which is formalized in WAYBEL20 [44] as

theorem                                                 :: WAYBEL20:34
for I being non empty set,
    J being RelStr-yielding non-Empty reflexive-yielding 
                                                    ManySortedSet of I
 st for i being Element of I holds J.i is continuous complete LATTICE
  holds product J is continuous;

The hint for the proof given in [25,  p. 60] suggests using the equational characterization of continuous lattices:

Since all operations in the cartesian product are component-wise, then any equation which holds in each factor holds in the product. Since the product of complete lattices is complete, 2.3 proves the claim.

We will not quote the entire Theorem 2.3 here, but suffice it to say that it involves distributivity equations of the form

$${\textstyle\bigwedge}_{j\in J} {\textstyle\bigvee}_{k\in K(j)... ...yle\bigvee}_{f\in M} {\textstyle\bigwedge}_{j\in J} x_{j,f(j)},$$

where $M$ is the set of functions defined on $J$ with values $f(j)\in K(j)$. Such equations are notoriously tedious to work with formally and thus we ended up proving Theorem 2.7 directly from the definition of the continuous lattice which seemed much simpler. If MIZAR has been better equipped with tools for handling algebra, we probably would have followed the hint from the book.