@MISC{WAYBEL_5.MIZ,
  AUTHOR = {\.Zynel, Mariusz},
  TITLE = {The Equational Characterization of Continuous Lattices},
  NOTE = {This work was partially supported by
   the Office of Naval Research Grant N00014-95-1-1336.},
  ACKNOWLEDGEMENT = {The author is greatly indebted to Grzegorz
    Bancerek for his inspiring influence during the preparation
    of this paper. Thanks are also due to the whole Mizar team in
    Bia{\l}ystok for collaboration.},
  SECTION1 = {The Continuity of Lattices},
  SECTION2 = {Completely-Distributive Lattices},
  SECTION3 = {Sub--Frames of Continuous Lattices},
  DAY = {25},
  MONTH = {October},
  YEAR = {1996},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {The class of continuous lattices can be characterized
    by infinitary equations. Therefore, it is closed under the
    formation of subalgebras and homomorphic images.  Following
    the terminology of \cite{Johnstone} we introduce a continuous
    lattice subframe to be a sublattice closed under the formation
    of arbitrary infs and directed sups. This notion corresponds with a
    subalgebra of a continuous lattice in \cite{CCL}.\par
    The class of completely distributive lattices is also introduced
    in the paper. Such lattices are complete and satisfy the most
    restrictive type of the general distributivity law. Obviously each
    completely distributive lattice is a Heyting algebra. It was hard
    to find the best Mizar implementation of the complete distributivity
    equational condition (denoted by CD in \cite{CCL}). The powerful
    and well developed Many Sorted Theory gives the most convenient
    way of this formalization.  A set double indexed by $K$, introduced
    in the paper, corresponds with a family
    $\{x_{j,k}: j\in J, k\in K(j)\}$. It is defined to be a suitable many
    sorted function. Two special functors: $\rm Sups$ and $\rm Infs$ as
    counterparts of $\rm Sup$ and $\rm Inf$ respectively, introduced in
    \cite{YELLOW_2.ABS}, are also defined. Originally the equation
    in Definition~2.4 of \cite[p.~58]{CCL} looks as follows:
    $${\textstyle\bigwedge}_{j\in J} {\textstyle\bigvee}_{k\in K(j)} x_{j,k} =
       {\textstyle\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)$. }}

