Lattices with topology

Topologies on posets induced by their ordering and, conversely, partial orders on topological spaces generated by their topologies are of central importance to the theory of continuous lattices. Examples of such topologies are: the Scott topology, introduced in the CCL-book as the family of sets which are inaccessible by directed sups; the lower topology, generated by complements of principal filters as subbasic open sets; and the Lawson topology, the common refinement of both.

When investigating such topologies, we need to address the matter from two perspectives simultaneously: the algebraic (lattice) perspective and the topological spaces perspective. In the case of the Lawson topology, we have to deal with three topologies and a poset at the same time. The solution from the CCL-book introduces new notations like Scott open, Scott closed, Scott neighborhood, etc. Although, it is possible to do the same in MIZAR, such types of notations which are not consistently used in the CCL-book, would unnecessarily complicate the use of general topology notions already developed in MML and require many new attributes. The problem was solved by employing multi-prefixed structures.

The root structure for topological spaces given in PRE_TOPC [41] is

definition
struct (1-sorted) 
 TopStruct (# carrier -> set,
              topology -> Subset-Family of the carrier #);
end;

and a relation is added to it in WAYBEL_9 [34] to obtain

struct (TopStruct, RelStr)
 TopRelStr (# carrier -> set,
              InternalRel -> (Relation of the carrier),
              topology -> Subset-Family of the carrier #);

An auxiliary mode defined in YELLOW_9 [11] captures the fact that a topology was added to a relational structure

definition
 let R be RelStr;
 mode TopAugmentation of R -> TopRelStr means       :: YELLOW_9:def 4
  the RelStr of it = the RelStr of R;
end;

The structure TopRelStr is both the structure TopStruct and the structure RelStr, so to an object of type TopRelStr one can apply attributes defined for posets as well as attributes defined for topological spaces.

If X is a TopRelStr, then we also have the following equality

the RelStr of X = RelStr(# the carrier of X, the InternalRel of X #)

and a similar one holds for TopStruct. The structure TopRelStr provides the ``building blocks'' for introducing a mode of lattices with topology in WAYBEL_9 [34]

definition
 mode TopLattice is with_suprema with_infima reflexive transitive
                    antisymmetric TopSpace-like TopRelStr;
end;

Note that TopLattice is a more general notion than a topological lattice since the continuity of meet and join operators is not required.

The attribute open is defined for subsets of TopStr as

definition let T be TopStruct, P be Subset of T;
  attr P is open means                               :: PRE_TOPC:def 5  
   P in the topology of T;
end;

and is applicable to a subset of any structural type widening to TopStr.

The Scott topology is a topological space having the following property

definition let T be reflexive non empty TopRelStr;
 attr T is Scott means                               :: WAYBEL11:def 4
  for S being Subset of T holds S is open iff S is inaccessible upper;
end;

In order to say that a subset of the carrier of TopRelStr is Scott open, we use the attribute open together with the attribute Scott and similarly for Lawson open (see Section ).

As an example of this approach, let us look at Proposition 1.6 from [25, p. 144].

1.6. Proposition. Let L be a complete lattice.

(i)

An upper set U is Lawson open iff it is Scott open;

(ii)

A lower set is Lawson-closed iff it is closed under sups of directed sets.

The corresponding MIZAR theorems appear in WAYBEL19 [12].

The MIZAR formalization of the if case of (i) was also formulated in a different way since every Scott open set is also upper by definition, and thus we have two theorems for (i) shown below, and only one theorem for (ii).

theorem                                                 :: WAYBEL19:37
 for S being Scott complete TopLattice,
     T being Lawson correct TopAugmentation of S,
     A being Subset of S 
  st A is open
   for C being Subset of T st C = A holds C is open;

theorem :: 1.6. PROPOSITION (i), p. 144                 :: WAYBEL19:41 
 for S being Scott complete TopLattice,
     T being Lawson correct TopAugmentation of S,
     A being upper Subset of T 
  st A is open
   for C being Subset of S st C = A holds C is open;

theorem :: 1.6. PROPOSITION (ii), p. 144                :: WAYBEL19:42
 for T being Lawson (complete TopLattice), A being lower Subset of T 
  holds A is closed iff A is closed_under_directed_sups;