@MISC{WAYBEL11.MIZ,
  AUTHOR = {Trybulec, Andrzej},
  TITLE = {{S}cott Topology},
  NOTE = {This work was partially supported by
   the Office of Naval Research Grant N00014-95-1-1336.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Scott Topology},
  SECTION3 = {Scott Convergence},
  DAY = {29},
  MONTH = {January},
  YEAR = {1997},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {In the article we continue the formalization in Mizar of \cite[98--105]{CCL}.
We work with structures of the form
 $$L =  \langle C,\ \leq,\ \tau \rangle,$$
where $C$ is the carrier of the structure,
 $\leq$ - an ordering relation on $C$ and
 $\tau$ a family of subsets of $C$.
When $\langle C,\ \leq \rangle$ is a complete lattice
we say that $L$ is Scott, if $\tau$ is the Scott topology
of $\langle C,\ \leq \rangle$.
We define the Scott convergence (lim inf convergence).
Following \cite{CCL} we prove that
in the case of a continuous lattice $\langle C,\ \leq \rangle$
the Scott convergence
is topological, i.e. enjoys the properties: (CONSTANTS), (SUBNETS),
(DIVERGENCE), (ITERATED LIMITS). We formalize the theorem, that if
the Scott convergence has the (ITERATED LIMITS) property,
the $\langle C,\ \leq \rangle$
is continuous.}}

