Mixing Order and Topology

Topologies on posets induced by the ordering and, conversely, partial orders on topological spaces generated by topology are investigated in the theory of continuous lattices. For example, Scott topology introduced in the compendium is the family of sets which are inaccessible by directed sups. Lawson topology and lower topology are another example of such topologies. Lawson topology is the common refinement of Scott and lower topologies and lower topology is generated by complements of principal filters as subbasic open sets.

When investigating such topologies we need to use both theories: posets and topological spaces. In the case of Lawson topology we have in the same time three topologies and a poset. The solution from the compendium consists in introducing new notation like Scott open, Scott closed, Scott neighbourhood, etc. It is possible to do the same in MIZAR but such notation causes substantial technical difficulties with the use of general topology developed in the MML. Besides, such notation is not consequently applied in the compendium.

The problem was solved by multi prefixed structure definition in [11] and by mode definition in [5].

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

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

TopStruct has two fields: carrier and topology and is the base structure of topological spaces. The structure TopRelStr is both the structure TopStruct and the structure RelStr. We may apply to it attributes defined for posets and attributes defined for topological spaces as well. If X is TopRelStr, then the RelStr of X will be strict RelStr and, moreover,

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

(analogically, for TopStruct).

:: WAYBEL_9
definition
 mode TopLattice is with_join with_meet reflexive transitive
         antisymmetric TopSpace-like TopRelStr;
end;

As an illustration of applied convention, let us compare the proposition 1.6 from the compendium, page 144, and corresponding MIZAR theorems.

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.

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

The implication from right to left in point (i) is proved in more general case:

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