Continuous Lattices

The concept of directed sets was changed in MIZAR formalization. A directed set is non empty in mathlore and in the compendium. However, it happens often that we need a set which is directed or empty. MIZAR does not allow to write a type as directed or empty set and we decided to formalize the concept as follows:

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

The theorem explaining correspondence to usual meaning has been proved also.

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
  proof .... end;

The concept of completeness presented in [7] depends on a context. A complete poset, complete semilattice, and complete lattice satisfy different conditions. In MIZAR we introduced attributes

• up-complete as completeness with respect to directed sups,
• inf-complete as completeness with respect to non empty infs,
• complete as completeness with respect to all sups.

Then, in MIZAR notation

Compendium	MML
a complete poset	up-complete Poset
a complete semilattice	inf-complete up-complete Semilattice
a complete lattice	complete LATTICE.

The fact that a complete lattice is a complete poset and a complete semilattice is expressed in MIZAR (see [3]) by conditional cluster registration:

 definition
   cluster complete -> up-complete inf-complete (non empty reflexive RelStr);
   coherence
    proof
      let R be non empty reflexive RelStr;
      assume R is complete;
      ....
      thus R is up-complete by ...
      ....
      thus R is inf-complete by ...
    end;
 end;

The conditional registration is used automatically by MIZAR. Attributes up-complete and inf-complete are added to a type when it widens to non empty reflexive RelStr and already includes attribute complete. The concept of continuous lattices presented in the compendium depends on context. We decided to formalize it in as general way as possible because all meanings of it may be expressed by the basic continuous attribute and some extra conditions of completeness.

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;

The attribute satisfying_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 is the supremum operation, see [2]. The waybelow x is a set of all elements of L which are way below x, see [4].

The MIZAR notation for continuous posets:

Compendium	MML
a continuous poset	continuous up-complete Poset
a continuous semilattice	continuous up-complete Semilattice
a complete-continuous	continuous inf-complete
semilattice	up-complete Semilattice
a continuous lattice	continuous complete lattice

As the test of the correctness of the introduced concepts, the correspondence between locally compact topological spaces and continuous lattices has been proved. 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 from space T ordered by inclusion.