A Compendium of Continuous Latti es

inFormalizing re ent mathemati s

Mizar

Grzegorz Ban erek (ban erekmizar.org) 

Institute of Computer S ien e, Bialystok Te hni al University, Poland and Dept. ofInformation Engineering, Shinshu University, Nagano, Japan.

Piotr Rudni ki (piotr s.ualberta. a) y

Dept. of Computing S ien e, University of Alberta, Canada.

MizarThis paper reports on theformalization of the theory of ontinuous latti es as presented in A Compendium of Continuous Latti es, [25℄. By
theformalization we mean a formulation of theorems, de nitions, and proofs
written in thelanguage whose orre tness is veri ed by the
pro essor.
This e ort was originally motivated by the question of whether or not thesystem was suÆ iently developed for the task of expressing advan ed mathemati s.
The urrent state of the formalization|57
arti les written by 16 authors|indi ates that in prin iple thesystem has su essfully met the hallenge.
To our knowledge it is the most sizable e ort aimed at me hani ally he king some
substantial and relatively re ent eld of advan ed mathemati s. However, it does notmean that doing mathemati s inis as simple as doing mathemati s traditionally (if doing mathemati s is simple at all). The work of formalizing the materialof [25℄ has: (i) prompted many improvements of theproof he king system;(ii) aused numerous revisions of the thedata base; and (iii) ontributed to
the \to do" list of further hanges to thesystem.
Abstra t.

Mizar

Mizar

Mizar

Mizar

Mizar

Mizar

Mizar qed

Mizar
Mizar

Mizar

Mizar

,
proje t, formalization of mathemati s, set theory, proof
he king, theory of ontinuous latti es, mathemati al knowledge management

Keywords:

mml { Mizar Mathemati al Libraryl { A Compendium of Continuous Latti es [25℄Abbreviations:This paper is dedi ated to all the Mizar authors and in parti ular to
the remaining parti ipants in the formalization of l:Czeslaw Bylinski, Noboru Endou, Adam Grabowski, Ewa Gradzka,
Jaroslaw Gryko, Artur Kornilowi z, Beata Madras, Agnieszka Julia
Marasik, Robert Milewski, Adam Naumowi z, Yuji Sakai, Bartlomiej
Skorulski, Andrzej Trybule and Mariusz Zynel.
_

May 25, 2002
Partially supported by JSPS P00025.
y Partially supported by NSERC Grant OGP9207 and Shinshu Endowment Fundfor Information S ien e.

2002 Kluwer A ademi Publishers. Printed in the Netherlands.

02jar.tex; 25/05/2002; 14:42; p.1

2

G. Ban erek and P. Rudni ki

Table of Contents

1
2
3
4

5

6
7
8
A

Introdu tion
Goals and Motivation
Logisti s
The ba kground material: mml and the YELLOW series
4.1 mml
4.2 Latti es in mml
4.3 mml revisions
4.4 The YELLOW series
4.5 Produ ts
4.6 Moore{Smith onvergen e
4.7 Con rete ategories
The main ourse: the WAYBEL series
5.1 Latti es
5.2 Galois onne tions
5.3 Continuous latti es
5.4 Algebrai latti es
5.5 Putting together order and topology
5.6 Alexander's lemma
5.7 The S ott topology
5.8 The Lawson topology
5.9 Duality theory
The length of formal texts, osts
Some other statisti s
Con lusions
The l-book|WAYBEL orresponden e

3
5
7
9
10
10
16
18
19
21
24
27
27
27
30
34
37
41
44
46
47
50
51
53
60

02jar.tex; 25/05/2002; 14:42; p.2

Continuous Latti es in

Mizar

3

1. Introdu tion

The Mizar language, developed by Andrzej Trybule from Universityof Bialystok , is a language used for the pra ti al formalization ofmathemati s. The main goal for the original design of Mizar was toreate a formal system lose to the mathemati al verna ular used inpubli ations with the requirement that the language be simple enoughto enable omputerized pro essing, in parti ular me hani al veri ationof orre tness. The ontinual development of Mizar has resulted in alanguage, software for he king the orre tness of texts written in thelanguage, numerous utility programs, a entrally maintained library ofmathemati s, and an ele troni hyper-linked journal, all available on
the Internet1 . Introdu tory information on Mizar an be found in [46℄and [17℄ (an interesting personal a ount is in [58℄). For the rest of thispaper, we assume that the reader is at least super ially familiar withthese basi texts. However, to set the tone for the main body of thepaper we start with some general remarks about the Mizar system.
The Mizar style of formalization provides some freedom of expression, but the required rigor assures that the result of the formalization
has a unique meaning. When formalizing a theory we introdu e de nitions, lemmas, and theorems hoping that they will be useful for future
developments. This is the essential idea behind developing the Mizar
data base.
The Mizar language is an attempt to approximate mathemati al
verna ular in a formal language. There are only 102 reserved words
forming a tiny subset of English words whi h are frequently used in regular mathemati al papers. The logi of Mizar is lassi al and the proofs
are written in the Fit h-Jaskowski style (see [29℄). De nitions allow for
the introdu tion of onstru tors for types, terms, adje tives, and atomi
formulae. Proofs onsist of a sequen e of steps, ea h step justi ed by
fa ts proved in earlier steps or separate lemmas, theorems, or s hemesof theorems. The Mizar veri er he ks whether ea h inferen e step isin its opinion obvious unlike other systems whi h rely on a xed setof inferen e or rewriting rules. The notion of an obvious inferen e has
been addressed in the past by M. Davis [22℄, P. Rudni ki [43℄, the Kiev
proje t [23℄, and more re ently by H. Friedman [24℄.
In the earlier stages of the Mizar proje t, there were plans to test
the Mizar system by building libraries based on various axiomati s:
ZFC for \normal" mathemati s, Peano axioms for theoreti al arithmeti , et . Be ause of the substantial e ort needed to build su h libraries, a de ision was made around 1988 to fo us on developing onea1

http://www.mizar.org

02jar.tex; 25/05/2002; 14:42; p.3

4
G. Ban erek and P. Rudni ki
su h library|Mizar Mathemati al Library (mml)|based on the Tarski-Grothendie k set theory.
We would like to stress the distin tion between Mizar as a formal
system of general appli ability (whi h as su h has little in ommon
with any set theory) and the spe i appli ation of Mizar in developing
mml whi h is based entirely on a set theory (see [48℄). In building mml,
the Mizar language and set theory provide an environment in whi h
all further mathemati s is developed. This development is de nitional :new mathemati al obje ts an be de ned only after supplying a modelfor them in the already available theories.
Mizar provides some elements of se ond order logi using s hemesof theorems. S hemes are expressed with free se ond order variables
and thus may be used to formulate indu tion s hemes, for example.
Multi pre xed stru tures allow us to introdu e algebrai on epts,
for example topologi al groups whi h are both groups and topologi al
spa es; the a ount of basi algebrai stru tures developed in Mizar
is given in [45℄.
The tools in the Mizar software olle tion support some typi altasks of doing mathemati s:developing and managing mathemati al knowledge,
verifying logi al orre tness of reasonings,
beautifying Mizar texts, e.g., nding irrelevant premises of aninferen e step or dis overing unused text items,presenting Mizar texts using TEX and HTML.
The development of mml2 has been the main a tivity of the Mizar
proje t sin e the late 1980's as it has been believed within the proje tteam that only substantial experien e may help in improving the system. Freek Wiedijk noti ed in [59℄:A good system without a library is useless. A good library for abad system is still very interesting (the system might be improvedor the library might be ported to a di erent, better system). So thelibrary is what ounts.

One of the largest on entrated e orts in developing mml has been
the formalization of A Compendium of Continuous Latti es [25℄ in its
entirety. This proje t3 started in 1996 and we report the state of thisb

2

See http://mizar.org
In the sequel our proje t will be referred to as the \proje t" or simply\ " while the book [25℄ will be frequently referen ed as \the-book". We areaware that the authors of [25℄ are preparing a new edition of the-book; however,it was not available at the time of this writing.
3

l

l

l
l

02jar.tex; 25/05/2002; 14:42; p.4

Mizar5
endeavor as of April 2002. A smaller report on the proje t as of Mar h2000 appeared in [14℄.
Dana S ott has raised an interesting question of opyright. The lbook is opyrighted by Springer-Verlag. Are we violating any opyrights
by formalizing the book in Mizar? It is not lear to us but we hope notand suÆ e it to say that no part of the book has been opied verbatim.
The plan of this paper is as follows. In Se tion 2 we explain the
purpose of formalizing the l-book at all and the expe ted results.
Se tion 3 presents the logisti s of the proje t. The next se tion presents
the Mizar rendition of basi notions in the l-book and ba kgroundmaterial assumed by the authors of [25℄ for their readers. We elaborateon parts of this material that required substantial e ort to formalize.
Se tion 5 dis usses the issues en ountered while formalizing the main
body of the l-book. The next two se tions o er some data about
the length of the formal texts and estimates of the human e ort of thisproje t. Se tion 8 draws on lusions while also presenting our plans forthe future.
Continuous Latti es in

2. Goals and Motivation
Can we do formalization of advan ed mathemati s like this inluded in regular mathemati al monographs in the urrent proofhe king systems?

The above question was raised at the 2nd QED4 Workshop held in
Warsaw in 1995. In trying to answer this question we followed Ralph
Wa hter's suggestion to put Mizar under a stress test by starting
the formalization of A Compendium of Continuous Latti es [25℄ in its
entirety. The proje t oÆ ially started in April 1996. The theory of
ontinuous latti es presented in [25℄ is a relatively re ent and a wellestablished eld; it is mathemati ally advan ed and involves a varietyof areas: algebra, general topology, analysis, ategory theory, logi ,topologi al algebra, and also tou hes on the theory of omputation.
The hoi e turned out to be a lu ky one. Foremost, the ompendium isvery rigorous whi h made the formalization omparatively easy (this isa hindsight view). Also, some initial fragments of the theory of latti es
had been already developed in Mizar (see Se tion 4.2).
In the past, there were some attempts to formalize entire mathemati al books in omputerized proof- he king systems. The best known
example was done in the 1970's when L. S. Jutting formalized Landau's Grundlagen der Analysis in de Bruijn's AUTOMATH system4

http://www-unix.m s.anl.gov/qed

02jar.tex; 25/05/2002; 14:42; p.5

6
G. Ban erek and P. Rudni ki(see [31, 35, 40℄). We are sure that in other proof assistants, people have been undertaking similar e orts of formalizing mathemati albooks, but we are aware of only two partially ompleted attempts:
D. L. Simon in his 1990 PhD thesis at University of Texas at Austin
he ked The elementary theory of numbers by Leveque using the BoyerMoore prover, and in the 1980's, J. Siekmann's group from Saarbru ken
started he king Dussen's Halbgruppen und Automaten with the helpof the MKRP prover.
Also in the 1980's, there was an attempt to formalize two haptersof Theoreti al Arithmeti by Grzegor zyk [28℄ in an earlier versionof Mizar alled Mizar-2 by a team led by A. Trybule . In Mizar2, ea h text was self ontained as there was no library. As a onsequen e, all ba kground knowledge needed to verify a text was put intoa preliminary se tion whi h was he ked only for synta ti orre tness.
Sin e 1989, the fo us of the Mizar proje t has been the developmentof a knowledge base alled Mizar Mathemati al Library (mml), a olle tion of texts written in the Mizar language alled Mizar arti les.
New Mizar arti les an be submitted to mml if they are a epted by
the Mizar veri er and refer only to arti les that already have been
in luded in mml. The starting point of mml onsisted of two axiomati
arti les:Tarski Grothendie k set theory in TARSKI [48℄, ontaining the axioms of Zermelo-Fraenkel set theory with the axiom of in nity
repla ed by Tarski's axiom on the existen e of arbitrarily strong
ina essible ardinals (axiom of hoi e is then proven as a theorem);
Built-in on epts in AXIOMS [49℄, ontaining axiomati s of strong
arithmeti of real numbers.
The latter arti le be ame a regular Mizar arti le in 1998 when the
onstru tion of real numbers was ompleted (in the ARYTM series of artiles [10, 54, 55, 37℄). Thus the fundamental properties of real numbers
be ame proven theorems rather than axioms, but the arti le is still
named AXIOMS ausing some onfusion for new omers.
Table I gives some quantitative data about mml at the start of thel proje t and at the time of this writing. In this table, an externalreferen e is a referen e from a Mizar arti le to another arti le in mml.
Any experiment with formalization of an entire book has many aspe ts and before starting l we expe ted to get answers or at least
some insight into the following:
Is the Mizar language suÆ iently expressive to formulate de nitions, theorems, and proofs ontained in the l-book?

02jar.tex; 25/05/2002; 14:42; p.6

Continuous Latti es inTable I.

mml: now and thenApril '96
April '02

Mizar

7

Arti lesSize
in kbytes

Theorems

De nitions

Externalreferen es

425
717

25,11852,18522,86331,741

4,193
6,093

163,999371,795

Is mml ri h enough to even start the formalization? To what degree does mml over the knowledge assumed in the l-book as
ba kground?
To what degree an di erent on epts already de ned in independent arti les in mml be used together?
Is the Mizar software apable of handling this amount of material?
What is the human e ort required for su h a formalization?
We hoped that running su h an experiment, irrespe tive of the answers
to the above questions, would lead to an improvement of Mizar sin e
all of the development team members were also involved in the lproje t and would work on the ne essary hanges. The urrent development team in ludes: G. Ban erek, Cz. Bylinski, A. Kornilowi z,
A. Naumowi z, and A. Trybule .
3. Logisti s

The work performed on the formalization of the l-book is the result of a team e ort by resear hers and students of the University ofBialystok with some ontributions from members in Canada and Japan.
In the summer of 1995, a seminar devoted to the theory of ontinuous
latti es based on [25℄ and [30℄ overed the material to be formalized andin the spring of 1996 the a tual work of formalization began. Grzegorz
Ban erek volunteered to lead the l proje t from the beginning andhas ontinued this leadership sin e. The list of all past and urrent
parti ipants omprises 16 authors listed below (in parentheses is thenumber of Mizar arti les ( o)authored in the l proje t and in theentire mml by ea h author):
Grzegorz Ban erek (19, 90), Czeslaw Bylinski (3, 36), Noboru Endou (2, 16), Adam Grabowski (4, 22), Ewa Gradzka (1, 2), Jaroslaw
Gryko (3, 6), Artur Kornilowi z (11, 45), Beata Madras (1, 7),

02jar.tex; 25/05/2002; 14:42; p.7

8

G. Ban erek and P. Rudni ki

Agnieszka J. Marasik (1, 4), Robert Milewski (8, 25), Adam Naumowi z (3, 11), Piotr Rudni ki (3, 43), Yuji Sakai (1, 3) Bartlomiej
M. Skorulski (2, 4), Andrzej Trybule (3, 86), Mariusz Zynel (2, 5).
The following rules were adopted at the outset of the proje t:
The formalization will be divided into two series of Mizar arti leswith identi ers pre xed by:_ YELLOW |arti les bridging the gap between the ontents of5and the knowledge assumed in the l-book,
 WAYBEL6|arti les formalizing the main ourse of the lbook.
No formalization of examples and exer ises will be done unlesssome item in the main text depends on it. This was meant to redu e
the workload as none of the parti ipants spe ialized in ontinuous
latti es.
The formalization should be as lose as possible to the l-book,
but provisions will be made for some Mizar pe uliarities su h as
built-in on epts and me hanisms, reuse of mml, and the like.
Whenever possible, the formalization should be more general thanthe l-book.
The work of formalization started by assigning parts of the rst two
hapters, O. A Primer of Continuous Latti es and I. Latti e Theoryof Continuous Latti es to individual team members. Be ause of thenumber of people involved, the work progressed in a di erent way thanthe usual sequential ontributions of arti les to mml. Usually, when an
author is writing an arti le, it is not available to other authors until
it is a epted to mml. We wanted to formalize di erent parts of thebook simultaneously as sequential development would be too slow. We
de ided to maintain a lo al data base of the YELLOW and WAYBEL series
to house ompleted and non- ompleted arti les. This allowed for someparallelism in the development of arti les. Arti les from the lo al librarywere tested by new arti les that used them and were revised as needed.
After some time they were presented at a seminar to dis uss possible
methods of generalization and nally submitted to mml. The rst arti les YELLOW 0 and WAYBEL 0 were submitted to mml on September 10
and September 12 of 1996, respe tively.
mml

5
6

Nobody remembers any good reason for sele ting this name.
The way below relation is the key on ept in ontinuous latti es, see Se tion 5.3.

02jar.tex; 25/05/2002; 14:42; p.8

Mizar9
It would be diÆ ult to de ne what onstitutes a Mizar arti leonsidered worthwhile for in lusion in mml. The nal de ision is with
the Library Committee ( urrently A. Grabowski and A. Kornilowi z),of the Mizar User's Asso iation whi h has a very liberal poli y fora epting arti les on e they are veri ed by the Mizar software. An
arti le is stored as a text- le and on average has (with median value
in parentheses): 1931 (1730) lines, 11,758 (10,435) tokens, 72.8 (62.2)
kbytes, and ontains 44.3 (37) theorems and 8.5 (6) de nitions. Theorems and de nitions in mml are te hni al terms and orrespond tomathemati al fa ts, no matter how simple or how deep.
The l-book ontains 334 pages, divided into 8 hapters ontaining a total of 715 items. The weight of items varies onsiderably. On
average, an arti le in the WAYBEL series overs 7 items, varying from 1
to 18 with a median of 5.
The formalization has been an e e tive stress test for the Mizar
software. It dete ted some errors in the software and for ed the adjustment of a number of quantitative parameters. The formalization
work would have not been possible without the ooperation of thesystem developers and the Library Committee who were responsiblefor improving the software and ondu ting a number of revisions ofmml, see Se tion 4.3.
Continuous Latti es in

4. The ba kground material: mml and the YELLOW series

The l-book embodies a blo k of advan ed mathemati s and assumes
a lot of ba kground knowledge of the readers. This posed two hallenges
for the l proje t.
Nobody in the team was spe ializing in ontinuous latti es although almost everyone had a general mathemati al ba kgroundat the MS 7 level. The team in luded two PhDs in mathemati s:
A. Trybule (topology) and G. Ban erek (logi ).
Before the a tual formalization started, we did not have a goodfeel for how mu h material already in mml ould be used in our
endeavor|it turned out that a substantial amount of su h material
des ribed in the remainder of the paper existed.

7

Parti ipation in the proje t for some authors onstituted the basis for their MS
degree.

02jar.tex; 25/05/2002; 14:42; p.9

104.1. mml

G. Ban erek and P. Rudni ki

has been under development sin e late 1988. By the time theproje t started, mml already had 422 arti les and overed, tovarying levels of detail, several quite diverse areas (see [46℄). mml isin essen e developed by \hobbyists" in the sense that only sporadi ally
there are suÆ ient funds available to organize larger teams for more
fo used e orts. In its initial years, l was one su h ase .
Most of mml ontained frequently used material overing the basi
mathemati al toolkit:
operations on sets, relations and fun tions,ordinal and ardinal arithmeti ,ordering and equivalen e relations,natural, integer, real and omplex numbers,
nite sequen es.
The following topi s of interest for the formalization of the l-bookwere overed in mml to some degree:
fundamental algebra: semigroups, monoids, groups, rings, elds,
modules, and ve tor spa es;
fundamental topology: basi de nitions, metri spa es, and disrete spa es;
posets and latti es, omplete latti es, and numerous instan es oflatti es.
It was not at all lear to what degree this material ould be used in its
original form for the l proje t, see Se tion 7 for some numbers.
mml
l

d

4.2. Latti es in mml
There are at least two approa hes to latti es in literature:
1. A latti e is an algebra with two binary operations t and u whi hsatisfy the onditions of idempoten e, asso iativity, ommutativity,
and absorption.
2. A latti e is a partially ordered set (poset) with suprema and in mafor non empty nite subsets.

02jar.tex; 25/05/2002; 14:42; p.10

Mizar11
Both approa hes were already present in mml and the orresponden e
between them has been proved. The l-book employs the se ond
approa h, but we brie y des ribe here how the rst approa h wasdeveloped in LATTICES [63℄ as it illustrates well a typi al way of working
with Mizar stru ture types.
The \mother" of almost all stru ture types is de ned in STRUCT 0 [36℄asContinuous Latti es indefinition
stru t 1-sorted(#end;arrier -> set #);The \ba kbone" stru tures for latti es are de ned as
definition
stru t(1-sorted) /\-SemiLattStr(# arrier -> set, L_meet -> BinOp of thestru t(1-sorted) \/-SemiLattStr(# arrier -> set, L_join -> BinOp of theend;arrier #);arrier #);definition
stru t(/\-SemiLattStr,\/-SemiLattStr) LattStr(# arrier -> set, L_join, L_meet -> BinOp of theend;arrier #);These de nitions are only the \building blo ks" without any latti e-like
properties. The LattStr stru ture merely ombines the elds of /\- and\/-SemiLattStr.
It is typi al to introdu e more onvenient notations for the semilatti e operations. In the remainder of this paper we omit all the proofs
whi h appear in Mizar arti les.
definition
let G be non empty \/-SemiLattStr, p,q be Element of the arrier of G;
fun p"\/"q -> Element of G equals:: LATTICES:def 1(the L_join of G).(p,q);
end;
definition
let G be non empty /\-SemiLattStr, p,q be Element of the arrier of G;
fun p"/\"q -> Element of G equals:: LATTICES:def 2(the L_meet of G).(p,q);
end;

The attributes to be applied to our \ba kbone" stru tures in order toform the on ept of a latti e are the following semi-latti e properties
definition let L be non empty \/-SemiLattStr;
attr L is join- ommutative means:: LATTICES:def 4

02jar.tex; 25/05/2002; 14:42; p.11

12

G. Ban erek and P. Rudni ki

for a, b being Element of the arrier of L holds a"\/"b = b"\/"a;attr L is join-asso iative means:: LATTICES:def 5
for a, b,being Element of the arrier of L
holds a"\/"(b"\/" ) = (a"\/"b)"\/" ;end;
definition let L be non empty /\-SemiLattStr;
attr L is meet- ommutative means:: LATTICES:def 6
for a, b being Element of the arrier of L holds a"/\"b = b"/\"a;attr L is meet-asso iative means:: LATTICES:def 7
for a, b,being Element of the arrier of L
holds a"/\"(b"/\" ) = (a"/\"b)"/\" ;end;

and to de ne absorption laws we need the entire latti e stru turedefinition let L be non empty LattStr;
attr L is meet-absorbing means:: LATTICES:def 8
for a, b being Element of the arrier of L holds (a"/\"b)"\/"b = b;
attr L is join-absorbing means:: LATTICES:def 9
for a, b being Element of the arrier of L holds a"/\"(a"\/"b) = a;end;

At this point, we an nally say what it means for a stru ture to belatti e-like.
definition let L be non empty LattStr;
attr L is Latti e-like means:: LATTICES:def 10
L is join- ommutative join-asso iative meet-absorbing
meet- ommutative meet-asso iative join-absorbing;end;

Next, we demonstrate that there are LattStrs whi h are Latti e-like;this is expressed by the following existential registrationedefinition
luster stri t Latti e-like (non empty LattStr);
end;

Assured of their existen e, we an nally introdu e the needed type forlatti es in the following expandable type de nition
definitionmode Latti e is Latti e-like (non empty LattStr);end;

Now we an prove properties of latti es, for example

reserve L for Latti e;reserve a, b,
for Element of thetheorem(for a,b,(for a,b,

arrier of L;:: LATTICES:19
holds a"/\"(b"\/" ) = (a"/\"b)"\/"(a"/\" ))iffholds a"\/"(b"/\" ) = (a"\/"b)"/\"(a"\/" ));02jar.tex; 25/05/2002; 14:42; p.12

Mizar13
However, it is quite typi al that for proving some latti e property we
do not need all the attributes of a latti e. In su h a ase, we use only
the required subset of attributes.
Continuous Latti es infor L being meet-absorbing join-absorbing meet- ommutative(non empty LattStr),a being Element of the arrier of L
holds a"\/"a = a & a"/\"a = a by LATTICES:17,18;

Of ourse, the above theorem works also for obje ts that share thesuper-set of the required attributes, for example all Latti e-like obje ts. One may de ne further attributes for latti es, su h as omplete or
distributive, and prove more interesting theorems (see LATTICES [63℄.)
The se ond of the earlier mentioned approa hes to latti es gives
wider usage, is easier to generalize (by weakening onditions of partial
ordering), and was the basi approa h in the l-book. Adopting thisapproa h as the basi one prompted the rst revision of mml whi honsisted in the generalization of posets and some latti e-theoreti alon epts (see Se tion 4.3).
RelStr is the base relational stru ture whi h serves as an an estor toquasi ordered sets, posets, semi-latti es, and latti es and is introdu ed( f. Se tion 4.3) in ORDERS 1 [56℄ as follows
definition
stru t (1-sorted) RelStr (#arrier-> set,InternalRel -> Relation of the
#);
end;

arrier

If R is a RelStr, then R is a stru ture with at least 2 elds: arrier
and InternalRel. A stru ture S an be a RelStr and may have more
elds when its type is derived from RelStr, i.e., when RelStr pre xes
the type of S . (The details of Mizar stru ture de nitions are presented
in [45℄.) The on ept of a poset was introdu ed in ORDERS 1 [56℄ after
rst de ning the needed attributes.
definition let A be RelStr;
attr A is reflexive means:: ORDERS_1:def 4
the InternalRel of A is_reflexive_in the arrier of A;
attr A is transitive means:: ORDERS_1:def 5
the InternalRel of A is_transitive_in the arrier of A;
attr A is antisymmetri means:: ORDERS_1:def 6
the InternalRel of A is_antisymmetri _in the arrier of A;
end;

The predi ates used in the de niens ome from RELAT 2 [62℄.

02jar.tex; 25/05/2002; 14:42; p.13

14

G. Ban erek and P. Rudni ki

reserve X, x, y, z for set;
definition let R, X;
pred R is_reflexive_in X means:: RELAT_2:def 1
x in X implies [x,x℄ in R;
pred R is_antisymmetri _in X means:: RELAT_2:def 4
x in X & y in X & [x,y℄ in R & [y,x℄ in R implies x = y;pred R is_transitive_in X means:: RELAT_2:def 8
x in X & y in X & z in X & [x,y℄ in R & [y,z℄ in R
implies [x,z℄ in R;
end;

Before de ning the Poset type we rst register the following existential
luster of attributesedefinition
luster non empty reflexive transitive antisymmetri
end;

stri t RelStr;

The above luster assures the existen e of an obje t of type RelStr withany subset of the listed attributes. Knowing that su h obje ts exist
we de nefdefinitionmode Poset is reflexive transitive antisymmetri
end;

RelStr;For onvenien e and to be loser to the usual notation, we introdu e
the following in x predi ate
definition
let R be RelStr, x, y be Element of thepred x <= y means[x,y℄ in the InternalRel of R;
synonym y >= x;
end;arrier of R;:: ORDERS_1:def 9

In order to de ne the on ept of a latti e based on a poset we need thefollowing attributes from LATTICE3 [4℄definition let R be RelStr;
attr R is with_suprema means:: LATTICE3:def 10
for x, y being Element of R
ex z being Element of R st x <= z & y <= z &for z' being Element of R st x <= z' & y <= z' holds z <= z';
attr R is with_infima means:: LATTICE3:def 11
for x, y being Element of R
ex z being Element of R st z <= x & z <= y &for z' being Element of R st z' <= x & z' <= y holds z' <= z;end;

Now we register the existen e of a luster of attributes

02jar.tex; 25/05/2002; 14:42; p.14

Continuous Latti es in

Mizar

15

definition
luster with_suprema with_infima stri t (non empty Poset);end;

and this delivers our poset based latti e. The orresponden e between
our new notion and Latti e is established with the help of the following
fun tors.
g

definition let L be Latti e;
fun LattRel L -> Relation equals{ [p,q℄ where p, q is Element of theend;:: FILTER_1:def 8
arrier of L: p"\/"q = q };definition let L be Latti e;
fun LattPOSet L -> stri t Poset equals
RelStr(#the arrier of L, LattRel L#);end;:: LATTICE3:def 2

For the orre tness of the latter de nition one needs to prove that
LattRel L is an Order on the arrier of L. LattPOSet enjoys the following properties.
theorem:: LATTICE3:6
for L1,L2 being Latti e st LattPOSet L1 = LattPOSet L2
holds the LattStr of L1 = the LattStr of L2;
theorem:: LATTICE3:11
for L being Latti e holds LattPOSet L is with_suprema with_infima;
theorem:: LATTICE3:19
for A being with_suprema with_infima non empty Poset
ex L being stri t Latti e st the RelStr of A = LattPOSet L;

The existen e in the last theorem is in fa t unique and thus we introdu ea third fun tor
definition
let A be RelStr su h that A is with_suprema with_infima Poset;
fun latt A -> stri t Latti e means:: LATTICE3:def 15
the RelStr of A = LattPOSet it;end;

The promised orresponden e between these two kinds of latti es is
nowhere expli itly stated in mml although it an be proven in a straightforward way as follows:
for P being stri t with_infima with_suprema Poset
holds LattPOSet latt P = P

by LATTICE3:def 15;

for L being stri t Latti e holds latt LattPOSet L = L
proof let L be stri t Latti e;

02jar.tex; 25/05/2002; 14:42; p.15

16

G. Ban erek and P. Rudni ki

LattPOSet L is with_suprema with_infima
by LATTICE3:11;
then LattPOSet latt LattPOSet L = LattPOSet L by LATTICE3:def 15;
hen e latt LattPOSet L = L
by LATTICE3:6;
end;

These two fa ts raise an interesting issue for any omputerized knowledge base for mathemati s: should the simple onsequen es of fa ts
already stored in the data base also be in luded in the data base? Thisis an important question for the pro ess of automating sear hes of thedata base. If one answers
yes: this would lutter the data base with a lot of trivialities,
no: there is overwhelming eviden e that su h simple onsequen es
are sometimes not that simple for humans to nd.
Probably a good solution would be to have the sear h engine generate su h simple onsequen es on the y. This would require somereasonably modest de nition of simple onsequen e in order to urb
the omplexity of sear hing algorithms.
4.3. mml revisions
mml frequently undergoes revisions whi h hange the arti les alreadyin it. Most hanges are small but sometimes there are substantial modi ations. A revision of the \past" is usually exe uted be ause withhindsight a better way is found to solve some problems. Here we would
like to des ribe one su h revision whi h was for ed by the start of thel proje t, namely the modi
ation of some mml ontents to introdu e a few basi latti e related notions. The other reason for spending
some spa e in this paper on revisions is be ause of our onvi tion thatrevisions of the past will be unavoidable in any data base of formalized
mathemati s. Thus, su h types of data bases should be furnished witha means for automating the pro ess. However, we do not laim we havea solution to this problem|it is not as straightforward as it might
appear at rsthand and many mml revisions are performed by hand.
Before the start of the l proje t, mml did not in lude a suÆ iently
general and exible notion of a poset. In ORDERS 1 [56℄, a stru ture forposets was de ned8
definition
stru t poset (#arrier -> non empty set,order -> Order of the arrier
8This an be still seen in [56℄, see the note on the referen es toon p. 57.

Mizar arti les

02jar.tex; 25/05/2002; 14:42; p.16

Continuous Latti es in

Mizar

17

#)
end;

where Order of X is a re exive, antisymmetri and transitive Relationof X. This stru ture was de ned in 1990 and did not use the 1-sorted

stru ture as a pre x sin e the latter was not introdu ed until 1995 in
an mml revision.
The above stru ture is not exible: the onditions for Order ofare not split into the basi properties of re exivity, transitivity, andantisymmetry. Therefore, should the need arise for a de nition of aquasi-poset, for example, one would have to de ne another stru ture,develop its theory, and then make some sort of onne tion between an
antisymmetri quasi-poset and a poset. This approa h seemed to be adead end if we ever planned to get to latti es.
A de ision was made to revise ORDERS 1 and all arti les depending on
it by repla ing the existing poset stru ture by a new, more general one
whi h would allow for more onvenient, obje t-oriented derivations.
The de nition of the poset stru ture was repla ed by RelStr (seeSe tion 4.2, p. 13); the eld order was repla ed by InternalRel witha more general type Relation of the arrier. Attributes reflexive,
antisymmetri , and transitive (previously de ned to be appli able toa Relation) are now also de ned for RelStr. In order to take advantageof Mizar pro essing of these attributes, the following properties of
fun tors were registerededefinition let A be Poset;
luster the InternalRel of A -> Order-like;end;definition
let X be set;
let O be Order of X;
luster RelStr( #X, O #) -> reflexive transitive antisymmetri ;end;

Poset is then introdu ed as an expandable type (see Se tion 4.2, p. 14).
Before the hange of poset to Poset, four other arti les overing

theory of posets existed in mml and several other arti les used some minor lemmas and notions from ORDERS 1. Of ourse, hanges in ORDERS 1
in uen ed the orre tness of these arti les and some work was required
to: update the environment se tions of these arti les, repla e old notions
by the new ones, and renumber theorems. Fortunately, many of thesetasks ould be done almost me hani ally with a stream editor. Some
simple generalizations of many fa ts were also made, but this work had
to be done by hand.

02jar.tex; 25/05/2002; 14:42; p.17

18

G. Ban erek and P. Rudni ki

The ontinuation of the l proje t prompted a number of otherrevisions|too te hni al to des ribe here.

mml

4.4. The YELLOW series
Re all that the arti les in the YELLOW series are intended to over theba kground material assumed by the l-book. This series of 22 arti les(out of 57 total in the proje t) indi ates that mml was in onsiderably good shape for the formalization (see some numbers in Se tion 7). However, in order to ll the gap, the following topi s had to be
developed.
Relational stru tures
 substru tures: YELLOW 0, YELLOW 2, YELLOW 6  produ ts: YELLOW 1,
YELLOW 3, YELLOW10  bounds: YELLOW 0, YELLOW 5  duality: YELLOW 7
 isomorphism: YELLOW14.
Posets bounds, suprema and in ma: YELLOW 0  Boolean posets: YELLOW 1
 retra ts: YELLOW16.
Latti es omplete: YELLOW 0, YELLOW 2  the latti e of ideals: YELLOW 2
 Boolean: YELLOW 2, YELLOW 5  modular and distributive: YELLOW11
 latti e operations on subsets of a poset: YELLOW 4  topologi al:
YELLOW13.
Topology
 Moore{Smith onvergen e: YELLOW 6  Baire and sober spa es:
YELLOW 8  bases: YELLOW 9, YELLOW13, YELLOW15  augmentations
and re nements: YELLOW 9  Hausdor spa es: YELLOW12  produ ts, Ti honov theorem: YELLOW14, YELLOW17  retra ts: YELLOW16
 ompa tness: YELLOW19.
Category theory
 on rete ategories: YELLOW18  isomorphisms, equivalen e andduality: YELLOW18, YELLOW20, YELLOW21  latti e-wise: YELLOW21.
In the following subse tion, we dis uss a number of these topi s
whose development raised some interesting issues.

02jar.tex; 25/05/2002; 14:42; p.18

Continuous Latti es in

Mizar

19

4.5. Produ ts
Dealing formally with produ ts of families of sets is quite tedious workespe ially sin e everyday pra ti e tends to sweep ertain problems under the arpet. For instan e, asso iativity of the Cartesian produ t(X  Y )  Z = X  (Y  Z )is often taken for granted and both sides of the equality are treatedas being equal to X  Y  Z whi h is understood as a set of triples.
Formally, ea h of the three is a di erent entity although one an easily introdu e the obvious isomorphisms among them. mml o ers thefollowing means for dealing with produ ts of sets.
The binary Cartesian produ t is de ned in ZFMISC 1 [18℄ as a setof pairs.
definition let X1,X2;
fun [: X1,X2 :℄ means:: ZFMISC_1:def 2
z in it iff ex x,y st x in X1 & y in X2 & z = [x,y℄;end;

We have also produ ts of three sets [: X1,X2,X3 :℄ de ned as[:[:X1,X2:℄,X3:℄, and of four sets [: X1,X2,X3,X4 :℄ de ned as[:[:X1,X2,X3:℄,X4:℄.
The produ t of an arbitrary family of sets is de ned in CARD 3 [2℄.
definition let f be Fun tion;
fun produ t f -> set means:: CARD_3:def 5
x in it iff ex g being Fun tion st x = g & dom g = dom f &for x st x in dom f holds g.x in f.x;
end;

It is a bit surprising that despite some e orts at unifying the two notations (see FUNCT 6 [3℄), they have not been uni ed ompletely. It turns
out that trying to work with produ t <* X, Y *>, that is a produ t of asequen e of sets with length 2, needs quite an investment for developing
additional onstru tors orresponding to the ones already existing for[: X, Y :℄.
At the start of the proje t, mml ontained de nitions for produ ts for some algebrai stru tures (Abelian groups and universal algebras), but we had to de ne the produ t for relational stru tures
in YELLOW 1 [26℄02jar.tex; 25/05/2002; 14:42; p.19

20

G. Ban erek and P. Rudni ki

definition let I be set, J be RelStr-yielding ManySortedSet of I;
fun produ t J -> stri t RelStr means:: YELLOW_1:def 4
the arrier of it = produ t Carrier J &for x,y being Element of the arrier of it st x in produ t Carrier J
holds x <= y iff
ex f, g being Fun tion
st f = x & g = y &for i be set st i in I
ex R being RelStr, xi, yi being Element of R
st R = J.i & xi = f.i & yi = g.i & xi <= yi;
end;

where the set I plays the role of an index set and Carrier is de ned
in PRALG 1 [38℄definition
let J be set, A be 1-sorted-yielding ManySortedSet of J;
fun Carrier A -> ManySortedSet of J means:: PRALG_1:def 13
for j being set st j in J
ex R being 1-sorted st R = A.j & it.j = the arrier of R;
end;(see Se tion 4.2 for more details).
Introdu ing the notions is only a small part of the tedious job offormalization and before the notions an be used onveniently, one
has to prove quite a number of theorems giving the frequently usedproperties of the introdu ed notions. It is quite diÆ ult to foresee all of
the needed properties of these notions and thus their hara terizationis spread all over mml . Let us quote just one example of su h a fa t.
htheorem:: YELLOW16:38
for I being non empty set,
J, K being RelStr-yielding non-Empty ManySortedSet of I
st for i being Element of I holds K.i is SubRelStr of J.i
holds produ t K is SubRelStr of produ t J;

Similar to the produ t of two sets we have the produ t of two RelStrs
de ned in YELLOW 3 [33℄definition let X, Y be RelStr;
fun [: X, Y: ℄ -> stri t RelStr means:: YELLOW_3:def 2
the arrier of it = [: the arrier of X, the arrier of Y :℄ &the InternalRel of it =[" the InternalRel of X, the InternalRel of Y "℄;end;

where the produ t of two relations is also de ned in YELLOW 3 [33℄definition let P, R be Relation;
fun [" P, R "℄ -> Relation means:: YELLOW_3:def 1

02jar.tex; 25/05/2002; 14:42; p.20

Continuous Latti es in

Mizar

21

for x, y being set
holds [x,y℄ in it iff
ex p, q, s, t being set
st x = [p,q℄ & y = [s,t℄ & [p,s℄ in P & [q,t℄ in R;
end;

The same question we asked above for the produ t of two sets is also
appli able here: ould we have just one produ t for RelStr and express[: X,Y: ℄ as produ t <* X, Y *>? Probably the inertia of the Mizar
authors or la k of dis ipline is to be blamed for still having both of thesenotions. This situation indi ates the kind of housekeeping work needed
for maintaining a knowledge base for mathemati s, espe ially when thebase be omes sizable|mml is still minus ule from the viewpoint of adata base overing most of mathemati s.
Produ ts of topologi al stru tures are dis ussed in Se tion 5.5.
4.6. Moore{Smith onvergen e
The l-book uses Moore{Smith onvergen e lasses to justify that
the S ott topology is adequate for des ribing the required lim-inf onvergen e (see Se tion 5.7) in topologi al terms. This posed quite a hallenge for formalization in YELLOW 6 [52℄ as [25, pp. 101{102℄ makes onlya referen e to [32℄ and A. Trybule ended up onstru ting onvergen elasses in Mizar from s rat h.
In Moore{Smith onvergen e theory, the on ept of a net is a generalization of the on ept of a sequen e; nets are sometimes alled
generalized sequen es. A sequen e is a fun tion on ! (linearly orderedby in lusion) and its generalization onsists in a weakening of the ordering onditions on the index set, that is, the sequen e domain. Nets
are formalized in WAYBEL 0 [6℄ based on a new stru ture NetStr over S
whi h is derived from the relational stru ture RelStr by augmenting itwith a mapping from the indi es|the arrier of the RelStr|into thearrier of the stru ture S.
definition
let S be 1-sorted;
stru t(RelStr) NetStr over S (#arrier -> set,
InternalRel -> Relation of the arrier,mapping -> Fun tion of the arrier, the
#);
end;

arrier of S

The arrier of S is the set on whi h we want to dis uss a topology.
Note that the arrier of S is not a eld in NetStr as S is a parameterand not a stru tural an estor of NetStr.

02jar.tex; 25/05/2002; 14:42; p.21

22

G. Ban erek and P. Rudni ki

For a NetStr over S to be a net on the arrier of S it must be non
empty, the indi es must be dire ted, and the order must be transitive.
This is expressed by two expandable type de nitions in WAYBEL 0 [6℄definition let L be 1-sorted;
mode prenet of L is dire ted non empty NetStr over L;
end;definition let L be 1-sorted;
mode net of L is transitive prenet of L;
end;\Usual" sequen es satisfy all these onditions as ! is non empty andlinearly ordered by in lusion. Thus, ! is a dire ted set.
We present below the onvergen e of nets based on [32℄. Consider a
net of L, N. We say that net N is eventually in X if there is an upper
one of indi es with values of N in X. This is aptured by the Mizar
predi ate
definition
let L be non empty 1-sorted, N be non empty NetStr over L, X be set;
pred N is_eventually_in X means:: WAYBEL_0:def 11
ex i being Element of N st
for j being Element of N st i <= j holds N.j in X;
end;

Given a topologi al spa e T, a net of T is said to be onvergent toa point p of T i it is eventually in every neighborhood of x. Sin e
in general a net may onverge to more than one point, a fun tor for
denoting the set of all limits of a net is introdu ed.
definition let T be non empty TopSpa e, N be net of T;
fun Lim N -> Subset of T means:: YELLOW_6:def 18
for p being Point of T holds p in it iff
for V being a_neighborhood of p holds N is_eventually_in V;end;

We say that a net N is onvergent if Lim N is non empty. Now, we may
express the Moore{Smith on ept of a onvergen e lass where the key
question is ( f. [32, p. 73℄):
If C is a lass onsisting of pairs (S; s), where S is a net in X ands is a point, when there is a topology T for X su h that (S; s) 2 C
i S onverges to s relative to the topology T ?
The onditions that C must satisfy for su h a topology to exist arestated in [32, p. 74℄ (re ast informally in Figure 1) and every lasssatisfying these onditions is alled a onvergen e lass. Our problem
here is simple: in order to dis uss onvergen e lasses what should thedomain(s) of these nets be? There are no lasses in Mizar and thus

02jar.tex; 25/05/2002; 14:42; p.22

Continuous Latti es in(CONSTANTS) Constant nets
(SUBNETS) If a net

Mizar

23

onverge.

onverges, then so does ea h of its subnets.

(DIVERGENCE) If a net does notsubnet whi h does notonverge to some point, then it has aontain any subnets(ITERATED LIMITS) Iterations ofonverging to the point.

onvergent nets yield

onvergent nets.

Figure 1. Topologi al onvergen e onditions

we ould not follow the approa h from [32℄. The problem is in nding
a set big enough to serve as the domain of our nets su h that for any
C and T , we have C indu es T i T indu es C .
Fortunately, the Tarski-Grothendie k set theory available in mml
allows for the onstru tion of universal sets. In our ase, the smallest universal lass of a set is suÆ iently large. More spe i ally, thefollowing mode is used for onvergen e lasses of the arrier of S
(see YELLOW 6 [52℄ for details)
definition let S be non empty 1-sorted;
mode Convergen e-Class of S means
it = [: NetUniv S, the arrier of S :℄;end;:: YELLOW_6:def 21

where
definition let X be non empty 1-sorted;
fun NetUniv X means
for x holds x in it iff
ex N being stri t net of X st N = x &the arrier of N in the_universe_of theend;:: YELLOW_6:def 14
arrier of X;

and the universe of a set A is a set B having the {transitive losure of A as an element and satisfying the following onditions de ned
in CLASSES1 [1℄.
definition let B be set;
attr B is being_Tarski-Class means:: CLASSES1:def 2
B is subset- losed &(for X being set holds X in B implies bool X in B) &(for X holds X = B implies X, B are_equipotent or X in B);
end;

Given a onvergen e lass we an form a topologi al spa e as follows
definition let S be non empty 1-sorted, C be Convergen e-Class of S;
fun Convergen eSpa e C -> stri t TopStru t means :: YELLOW_6:def 27
the arrier of it = the arrier of S &02jar.tex; 25/05/2002; 14:42; p.23

24

G. Ban erek and P. Rudni ki

the topology of it ={ V where V is Subset of the arrier of S:
for p being Element of the arrier of S st p in V
for N being net of S st [N, p℄ in C holds N is_eventually_in V };end;

A onvergen e lass is alled topologi al if it satis es the onditions
stated in Figure 1. The key theorems then state thattheorem:: YELLOW_6:49
for S be non empty 1-sorted, C be Convergen e-Class of S
holds C = Convergen e Convergen eSpa e C;
theorem:: YELLOW_6:53
for T be non empty 1-sorted, C be Convergen e-Class of T
holds Convergen e Convergen eSpa e C = C iff C is topologi al;

The point that we would like to make here is this: fortunately for our
proje t, mml ontained the theory of Tarski universal lasses as without
it, the detour in formalizing the notion of a onvergen e lass and thus
S ott's topology (see Se tion 5.7) would have been mu h longer.
4.7. Con rete ategories
A ategory C is on rete if there exists a fun tion assigning to ea hobje t A of C its arrying set, the C - arrier of A, su h thata morphism in C from A to B is a fun tion from C - arrier of A to
C - arrier of B ,the omposition of morphisms is a fun tion omposition, andidentity morphisms are identity maps.
The formalization of on rete ategories in mml was motivated by
the duality theory for ontinuous latti es (see [25, p. 189℄). In duality
theory, we have to onsider various types of maps between latti es andit is natural to use the framework of ategory theory. Namely, we ope
with on rete ategories whose obje ts are latti es and morphisms aremaps preserving some latti e properties. For example, the base ategoryof this theory, the ategory UPS, has omplete latti es as its obje ts
and maps preserving dire ted suprema as morphisms. Other ategories
INF and SUP, also with omplete latti es as obje ts, have morphismspreserving in ma and suprema, respe tively.
The problem with formalizing su h notions lies again in the task of
expressing on epts from a set theory with lasses in the terminology
of a set theory without lasses, like the Tarski-Grothendie k set theory

02jar.tex; 25/05/2002; 14:42; p.24

Mizar25
sele ted for mml. For example, we annot de ne a ategory with all
omplete latti es as obje ts. In Mizar formalization, all obje ts ofa xed ategory must form a set and, be ause there is no set of all
omplete latti es, there is also no ategory of all omplete latti es (seeSe tion 5.9).
The Mizar formalization may be seen as more general and for es
investigations of di erent ategories, that is, ategories over di erent
sets of latti es. As a result, ategories with xed universa as in thel-book be ome one of the overed instan es. Fortunately, the theory
does not refer to the ri hness of these ategories and the fa t that they
are losed under some algebrai onstru tions does not a e t our work
now.
There are two approa hes in mml to the formalization of ategories.
The rst method proposed in CAT 1 [19℄ introdu es a stru ture withuniqueness of domain and odomain. Namely, the stru ture in ludes
elds Cod and Dom whi h are fun tions from morphisms to obje ts. So,
the on ept of a morphism from one obje t to another is de ned byvalues of Dom and Cod. In other words, the hom-sets are disjoint. The
on rete ategory Ens V of all sets from the family V and fun tions
among them was formalized in this approa h with morphisms as triples[[a, b℄, f℄, where f is Fun tion of a, b. In parti ular, morphisms of
Ens V are not fun tions and their omposition is expressed in a slightly
ompli ated way in ENS 1 [20℄.
Continuous Latti es indefinition let V be set, m1, m2 be Element of Maps V;
assumeod m1 = dom m2;
fun m2*m1 -> Element of Maps V equals[[dom m1, od m2℄, m2`2*m1`2℄;
end;:: ENS_1:def 7

This de nition is permissive, that is, its de niens is available only when
the assumed ondition is met. This means that we an use the expression m2*m1 freely and it always denotes an element of Maps V. However,what this term is equal to we an determine only when od m1 = dom
m2. Maps V is the set of morphisms of Ens V.
The se ond approa h, introdu ed in ALTCAT 1 [50℄, starts from theon ept of a morphism. Namely, AltCatStr has a eld Arrows whi h assigns to ea h pair of obje ts a set of morphisms. The EnsCat V ategory
is formalized as AltCatStr with Arrows assigning to any pair of sets theset of all fun tions from the rst set into the se ond. The ompositionof morphisms in EnsCat V is a omposition of fun tions. This approa hompli ates the on ept of fun tors and their omposition, but on theother hand it enables us to generalize fun tors.
The se ond approa h was hosen to introdu e a general frameworkfor on rete ategories and, eventually, latti e-wise ategories. A latti e-

02jar.tex; 25/05/2002; 14:42; p.25

26
G. Ban erek and P. Rudni ki
wise ategory is a on rete ategory C with latti es as obje ts andmonotone maps as morphisms. The arrying set of an obje t of C is thevalue of the arrier sele tor of the obje t, that is
for C being latti e-wise ategory, a being obje t of C
ex S being 1-sorted st S = a & C- arrier a = the arrier of S

In the urrent implementation, be ause it is impossible to rede nealled asting
fun tor was introdu ed for onvenien e.
obje t of to be RelStr or even 1-sorted, the following so

definition
let a be set;
fun a as_1-sorted -> 1-sorted equals
a if a is 1-sorted otherwise 1-sorted(# a #);end;:: YELLOW21:def 1

A suitable rede nition was made for obje ts of latti e-wise ategories
definition
let C be latti e-wise ategory, a be obje t of C;
redefine fun a as_1-sorted -> LATTICE equalsa;synonym latt a;end;:: YELLOW21:def 6

and another asting fun tor was de ned for de oding the ategorymorphisms to the latti e language.
definition
let C be latti e-wise ategory, a, b be obje t of C su h that<^a, b^> <> {};let f be Morphism of a,b;
fun f -> monotone map of latt a, latt b equals:: YELLOW21:def 7
f;end;

The two theorems below state the orresponden e of isomorphisms
expressed in terms of ategories and latti es.
theorem:: YELLOW21:4
for C being with_all_isomorphisms (latti e-wise ategory)a, b being obje t of C, f being Morphism of a,b
st f is isomorphi holds f is iso;theorem:: YELLOW21:5
for C being latti e-wise ategory,a,b being obje t of C st <^a, b^> <> {} & <^b, a^> <> {}for f being Morphism of a, b st f is iso holds f is isomorphi ;02jar.tex; 25/05/2002; 14:42; p.26

Mizar27
The isomorphi attribute is a notion about relational stru tures while
iso is from the world of ategories.
The ma hinery of ategories presented in this se tion was heavily
used in the formalization of duality (see Se tion 5.9).
Continuous Latti es in

5. The main ourse: the WAYBEL series

In this se tion, we will present a number of sele ted issues fa ed during
our proje t. Appendix A lists the parts of the l-book overed in ea hof the arti les of the WAYBEL series.
5.1. Latti es
In order to get the de nition of a latti e loser to that in the lbook, the de nitions of re exivity, transitivity, and antisymmetry wererede ned in YELLOW 0 [5℄ as in arnations of analogous notions from
ORDERS 1 [56℄ (see Se tion 4.2, p. 13).
idefinition let A be non empty RelStr;
redefine attr A is reflexive means
for x being Element of A holds x <= x;end;:: YELLOW_0:def 1

definition let A be RelStr;
redefine
attr A is transitive means:: YELLOW_0:def 2
for x,y,z being Element of A st x <= y & y <= z holds x <= z;
attr A is antisymmetri means:: YELLOW_0:def 3
for x,y being Element of A st x <= y & y <= x holds x = y;end;

YELLOW 0 also introdu es a host of similar de nitions whi h serve tobridge the state of mml and the requirements of formalizing the lbook. WAYBEL 0 [6℄ gives the nal version of the on ept of a latti easdefinitionmode Semilatti e is with_infima Poset;
mode sup-Semilatti e is with_suprema Poset;
mode LATTICE is with_infima with_suprema Poset;
end;

5.2. Galois onne tions
Galois onne tions are introdu ed in WAYBEL 1 [6℄ in two steps. First,
a mode for onne tions between two RelStrs is de ned to be a pair ofmaps followed by a onvenient rede nition .

02jar.tex; 25/05/2002; 14:42; p.27

28

G. Ban erek and P. Rudni ki

definition let S,T be RelStr;
mode Conne tion of S, T -> set means:: WAYBEL_1:def 9
ex g being map of S, T, d being map of T, S st it = [g, d℄;end;definition let S,T be RelStr, g be map of S,T, d be map of T,S;
redefine fun [g, d℄ -> Conne tion of S, T;
end;

Starting in this way, we an use the mode for purposes other than
only one spe ial kind of onne tion. Sin e our interest was in Galois
onne tions, the Galois attribute for Conne tion was introdu ed.
definition let S, T be non empty RelStr, g be Conne tion of S, T;
attr g is Galois means:: WAYBEL_1:def 10
ex g being map of S, T, d being map of T, S
st g = [g, d℄ & g is monotone & d is monotone &for t being Element of T, s being Element of S
holds t <= g.s iff d.t <= s;end;

Right after this de nition, a more onvenient formulation was statedin the following theorem.
theorem:: WAYBEL_1:9
for S,T being non empty Poset, g being map of S,T, d being map of T,Sholds [g, d℄ is Galois
iff g is monotone & d is monotone &for t being Element of T, s being Element of S
holds t <= g.s iff d.t <= s;

One may wonder why we need the theorem when we already have thede nition. The answer is: we do not; however, the se ond formulation
is more onvenient when:g and d are appropriate maps between T and S,[g, d℄ is Galois (that is, [g, d℄ is Conne tion of T, S due to theprevious rede nition), andwe would like to a ess the fa ts from the de niens of WAYBEL 1:def
10.
Be ause of the way the urrent version of Mizar works, all we an getin one step from WAYBEL 1:def 10 is an existentially quanti ed formula(whi h an be eliminated in the same step with the onsider onstru t)
and in order to pro eed, we have to use properties of equality of twoordered pairs. Using WAYBEL 1:9 instead frees us of this trouble. In theother dire tion, that is, from the de niens to the de niendum, both the

02jar.tex; 25/05/2002; 14:42; p.28

Mizar29
de nition and the theorem an be used in exa tly the same way. The
Mizar he ker is ontinually upgraded and one of the extensions being
onsidered may eliminate the di eren e des ribed above.
The names of adjoints are introdu ed using the same notation as in
the l-book.
Continuous Latti es indefinition let S, T be non empty RelStr, g be map of S, T;
attr g is upper_adjoint means:: WAYBEL_1:def 11
ex d being map of T, S st [g,d℄ is Galois;
synonym g has_a_lower_adjoint;
end;
definition let S, T be non empty RelStr, d be map of T, S;
attr d is lower_adjoint means:: WAYBEL_1:def 12
ex g being map of S, T st [g,d℄ is Galois;
synonym d has_an_upper_adjoint;
end;

Both of these de nitions ould have been written in one de nitional
blo k at the expense of some onfusion.
definition let S, T be non empty RelStr, g be map of S, T;
attr g is upper_adjoint means
ex d being map of T, S st [g, d℄ is Galois;
synonym g has_a_lower_adjoint;
attr g is lower_adjoint means
ex d being map of T, S st [d, g℄ is Galois;
synonym g has_an_upper_adjoint;
end;

The Mizar pro essor would not mind these expressions at all, but forhuman readers the ombined version would be rather puzzling.
The on ept of Galois onne tions is used to introdu e Heyting
algebras. Namely, a latti e is alled a Heyting algebra if for ea h of
its elements x, the map s 7! x u s has an upper adjoint ( f. De nition
3.17 in [25, p. 25℄). In other words, in a Heyting algebra an impli ation
is de nable.
The tasks of de ning a Heyting algebra and proving that an impliation an be de ned in it tested the orre tness of our formalizationof Galois onne tions.
definition let S be non empty RelStr, x be Element of S;
fun x"/\" -> map of S, S means:: WAYBEL_1:def 18
for s being Element of S holds it.s = x"/\"s;end;definition let H be non empty RelStr;
attr H is Heyting means
H is LATTICE &:: WAYBEL_1:def 19

02jar.tex; 25/05/2002; 14:42; p.29

30

G. Ban erek and P. Rudni ki

for x being Element of H holds x"/\"synonym H is_a_Heyting_algebra;
end;

has_an_upper_adjoint;

We needed some additional fun tors in order to onveniently formalize
the key theorem.
definition let H be non empty RelStr, a be Element of H;
assume H is Heyting;fun a=> -> map of H, H means:: WAYBEL_1:def 20[it, a"/\"℄ is Galois;
end;definition let H be non empty RelStr, a, y be Element of H;
fun a=>y -> Element of H equals:: WAYBEL_1:def 21
a=>.y;
end;

The rst de nition introdu es => as a unary post x operator and these ond de nes it as a binary operator. With the help of these fun tors
the key theorem is now expressed astheorem :: WAYBEL_1:70
for H being non empty RelStr st H is_a_Heyting_algebra
for x, a, y being Element of H holds x >= a"/\"y iff a=>x >= y;Galois onne tions are heavily used in duality theory (see Se tion 5.9).
5.3. Continuous latti es
The on ept of a dire ted set was hanged slightly in the Mizar formalization. A dire ted set is non empty in math-lore and in the l-book.
However, it happens frequently that we need a set whi h is dire ted or
empty. Mizar does not allow for the de nition of a dire ted or empty
set type and we de ided to formalize the on ept as follows
definition :: CCL, Definition 1.1, p. 2
let L be RelStr, X be Subset of L;
attr X is dire ted means:: WAYBEL_0:def 1
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;end;

The theorem explaining orresponden e to the usual meaning appears
astheorem:: WAYBEL_0:1
for L being non empty transitive RelStr, X being Subset of L
holds X is non empty dire ted
iff for Y being finite Subset of X
ex x being Element of L st x in X & x is_>=_than Y;

02jar.tex; 25/05/2002; 14:42; p.30

Mizar31
The on ept of ompleteness presented in the l-book depends
on ontext. A omplete poset, a omplete semi-latti e, and a omplete
latti e have to satisfy di erent onditions. In Mizar, we introdu ed
the following attributes:
up- omplete for ompleteness with respe t to dire ted sups,
Continuous Latti es in/\- omplete

for ompleteness with respe t to non empty infs,

omplete forompleteness with respe t to all sups.
Then, we have the following orresponden e
The

l

-book

mml

omplete poset
omplete semilatti eomplete latti e

up- omplete Poset/\- omplete up- omplete Semilatti eomplete LATTICE.

The fa t that a omplete latti e is both a omplete poset and aomplete semilatti e is expressed in WAYBEL 0 [6℄ by the onditional
luster registrationidefinition
luster omplete -> up- omplete /\- omplete(non empty reflexive RelStr);end;

The up- omplete and /\- omplete attributes are automati ally added
to an obje t already attributed by omplete when its type widens to anon empty reflexive RelStr.
Sin e the on ept of a ontinuous stru ture di ers for latti es, semilatti es, and posets in the l-book, we de ided to formalize it in as
general a way as possible by apturing the ommon meaning in thebasi ontinuous attribute (see WAYBEL 3 [7℄).
definition
let L be non empty reflexive RelStr;
attr L is ontinuous means:: WAYBEL_3:def 6(for x being Element of L holds waybelow x is non empty dire ted) &L is up- omplete satisfying_axiom_of_approximation;
end;

Note that our de nition of ontinuity orresponds to De nition 1.26,
p. 52 rather than De nition 1.6, p. 42 from the l-book. The attributeon erning the axiom of approximation is introdu ed as follows.

02jar.tex; 25/05/2002; 14:42; p.31

32

G. Ban erek and P. Rudni ki

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 fun tor is a supremum operator de ned in YELLOW 0 [5℄. The
waybelow x is a set of all elements of L whi h are way below x as
introdu ed by the following de nitions in WAYBEL 3 [7℄definition :: CCL 1.1, p. 38
let L be non empty reflexive RelStr, x,y be Element of L;
pred x is_way_below y means:: WAYBEL_3:def 1
for D being non empty dire ted Subset of L st y <= sup D
ex d being Element of L st d in D & x <= d;synonym x << y; synonym y >> x;
end;
definition :: after CCL 1.2, p. 39
let L be non empty reflexive RelStr, x be Element of L;
fun waybelow x -> Subset of L equals:: WAYBEL_3:def 3{y where y is Element of L: y << x};
fun wayabove x -> Subset of L equals:: WAYBEL_3:def 4{y where y is Element of L: y >> x};end;

Our nal notation for ontinuous stru tures is summarized below.
lontinuous poset
ontinuous semilatti eomplete- ontinuous
semilatti eontinuous latti emml

ontinuous up- omplete Poset
ontinuous up- omplete Semilatti eontinuous /\- omplete
up- omplete Semilatti eontinuous omplete latti e

As a test of the orre tness of the introdu ed on epts, we proved theorresponden e between lo ally ompa t topologi al spa es and ontinuous latti es (see l [25, p. 42℄). This orresponden e is expressedby two theorems
theoremfor T being non empty TopSpa e
st T is_T3 & In lPoset(the topology of T) is
holds T is lo ally- ompa t;:: WAYBEL_3:42
ontinuous

theorem:: WAYBEL_3:43
for T being non empty TopSpa e st T is lo ally- ompa tholds In lPoset(the topology of T) is ontinuous;

02jar.tex; 25/05/2002; 14:42; p.32

Mizar33
The In lPoset(the topology of T) is the poset of open sets of T with
set in lusion as the InternalRel.
The entire l-book is written very arefully and it is hard to nderrors of substan e. Sometimes, however, we found theorems whose
proofs as suggested in the l-book seemed too tedious to formalize
and we ended up with di erent proofs. A ase in point is the following
Continuous Latti es inj

2.7. Theorem. The lass of ontinuous latti es is losed under
the formation of arbitrary produ ts ...
(i) If L : j 2 J is a family of ontinuous latti es, then theartesian produ t X 2 L is a ontinuous latti e (relative tothe omponent-wise partial order);
j

j

J

j

from [25, p. 60℄ whi h is formalized in WAYBEL20 [44℄ astheorem:: WAYBEL20:34
for I being non empty set,
J being RelStr-yielding non-Empty reflexive-yielding
ManySortedSet of I
st for i being Element of I holds J.i is ontinuous omplete LATTICE
holds produ t J is ontinuous;

The hint for the proof given in [25, p. 60℄ suggests using the equational
hara terization of ontinuous latti es:
Sin e all operations in the artesian produ t are omponent-wise,
then any equation whi h holds in ea h fa tor holds in the produ t.
Sin e the produ t of omplete latti es is omplete, 2.3 proves thelaim.
We will not quote the entire Theorem 2.3 here, but suÆ e it to say thatit involves distributivity equations of the form
V W
= W 2 V 2 x ( );22 ( )xwhere M is the set of fun tions de ned on J with values f (j ) 2 K (j ).
Su h equations are notoriously tedious to work with formally and thus
we ended up proving Theorem 2.7 dire tly from the de nition of theontinuous latti e whi h seemed mu h simpler. If Mizar has been
better equipped with tools for handling algebra, we probably would
have followed the hint from the book.
j

J

k

K j

j;k

f

M

j

J

j;f j

02jar.tex; 25/05/2002; 14:42; p.33

34
G. Ban erek and P. Rudni ki
5.4. Algebrai latti es
Examples of algebrai latti es are latti es of ongruen es and latti es ofsubalgebras of an algebra; they are ontinuous. In formalizing this material, notational solutions di erent from those in the l-book [Ch. I,
Se tion 4℄ were adopted.
5.4.1. Subset of ompa t elements
The l-book de nes the subset K (L) of all ompa t elements of alatti e L and treats it as a set. The l-book does not make a lear
distin tion between a subset of a stru ture and a substru ture of thestru ture. A better solution for the formalization seemed to be theintrodu tion of a orresponding sublatti e in WAYBEL 8 [39℄ as
definition:: DEFINITION 4.1, p. 85
let L be non empty reflexive RelStr;
fun Compa tSublatt L -> stri t full SubRelStr of L means:: WAYBEL_8:def 1
for x being Element of L
holds x in the arrier of it iff x is ompa t;
end;

where full has the usual ategory theoreti meaning of restri ting theinternal relation to the arrier of the substru ture. Where the l-bookuses K (L), we write
thearrier of Compa tSublatt L

whi h at the time of its introdu tion seemed a better solution. If we
had introdu ed the following fun tor
fun

COMPACT L -> Subset of L

to play the role of K (L), then in many pla es we would have had touse expressions of the form
for K being SubRelStr st thearrier of K = COMPACT L holds ...

whi h do not read elegantly. It seems that using Compa tSublatt L
avoided this in onvenien e and by introdu ing appropriate fun torial
registrations for it, the me hanization of some reasoning steps be ame
possible.
However, in hindsight it now seems that working with just a set
and using Mizar luster me hanisms to arry the needed information
ould have been just as e e tive, if not better. With COMPACT de ned
above, we ould have used the fun tor subrelstr (de ned in YELLOW 0 [5℄and appli able to a subset of a stru ture) whi h re overs the full
substru ture of its argument. In that ase, instead of Compa tSublatti

02jar.tex; 25/05/2002; 14:42; p.34

35
L, we would have been working with subrelstr COMPACT L and insteadof the arrier of the former, we would have written just COMPACT L.
Another possibility would have been to de ne a host of term adje tive
registrations for subrelstr COMPACT L as the type of this term arries
all the information about L. However, that would be impossible for thearrier of Compa tSublatt L as its type is just set. An mml revision
may hange the urrent solution.
Continuous Latti es in

Mizar

5.4.2. Additional notation
The l-book very frequently uses the term # x \ K (L). While thisterm is not parti ularly ompli ated, we were afraid that we might run
into typing problems as rede nitions are deli ate onstru ts allowed
only for fun tors and not for terms. Therefore, the following shorthandnotation was introdu ed
definition
let L be non empty reflexive RelStr, x be Element of L;
funompa tbelow x -> Subset of L equals:: WAYBEL_8:def 2{ y where y is Element of L: x >= y & y is ompa t };end;

whi h substantially simpli ed further writing. The above de nition
employs the Fraenkel operator in its de niens. The Fraenkel operator
is very onvenient in de nitions sin e we do not have to prove existen e. However, using su h a de nition is rather tedious and thus amore onvenient hara terization of the de ned notion is expressed asa theorem.
theorem:: WAYBEL_8:4
for L be non empty reflexive RelStr, x, y be Element of L
holds y in ompa tbelow x iff x >= y & y is ompa t;# \The original x K (L) from the l-book is written as ompa tbelow
x and the following theorem shows that they are equivalent.
theorem:: WAYBEL_8:5
for L be non empty reflexive RelStr, x be Element of L holds
ompa tbelow x = downarrow x /\ the arrier of Compa tSublatt L;

5.4.3. A generalization
The notion of an algebrai latti e is generalized as
definition
let L be non empty reflexive RelStr;
attr L is satisfying_axiom_K means
for x be Element of L holds x = supend;:: WAYBEL_8:def 3
ompa tbelow x;

02jar.tex; 25/05/2002; 14:42; p.35

36

G. Ban erek and P. Rudni ki

definition:: DEFINITION 4.4, p. 85
let L be non empty reflexive RelStr;
attr L is algebrai means:: WAYBEL_8:def 4(for x being Element of L
holds ompa tbelow x is non empty dire ted) &L is up- omplete satisfying_axiom_K;
end;

Note the similarity between this de nition and de nitions of ontinuous
latti es and omplete latti es in Se tion 5.3. In all these ases, we use
the property of existen e of suprema of appropriate subsets rather thanusing the attribute omplete. With this generalization we an treat algebrai latti es whi h are not omplete, unlike the l-book whi h does
not provide for su h obje ts. Instead, the l-book proposes a separate
de nition of algebrai posets and semilatti es in an exer ise [25, Ch.
I, 4.28, p. 94℄. We nd the Mizar approa h more onvenient and wefollow it also for the ase of arithmeti latti es whi h we do not dis uss
here due to la k of spa e.
5.4.4. Stru ture typed lo i
We would like to make some omments on a ertain \obnoxious" property of the urrent implementation of Mizar on erning onstru tors
whose arguments are stru tures. The remarks below apply to all stru tures, but we will use algebrai latti es as an example. Currently, there
is a need to prove theorems of the following form
theorem:: WAYBEL_8:17
for L1, L2 be non empty reflexive antisymmetri RelStrst the RelStr of L1 = the RelStr of L2 & L1 is algebrai
holds L2 is algebrai ;The forgetful fun tor the RelStr of when given a stru ture derived
from a RelStr returns the stri t RelStr stru ture, that is, a stru turewith exa tly two elds: arrier and InternalRef. Be ause of this formulation, the theorem an be applied to obje ts of type, say, TopRelStr(see Se tion 5.5.1).
The attribute algebrai was de ned above for non empty reflexive
RelStr. One would suspe t that if the RelStr of L1 = the RelStr ofL2 and L1 is algebrai , then obviously L2 is also algebrai , but this is not
obvious to the Mizar he ker. In the ase of the attribute algebrai
as de ned above, it is really puzzling why not. However, in general,
the simplest of reasons for a theorem of this form not being obvious tothe he ker is that it an be false. For the sake of illustration, let us
onsider the following, simpli ed and twisted, example. First, we de ne
an attribute02jar.tex; 25/05/2002; 14:42; p.36

Continuous Latti es in

Mizar

definition
let R be RelStr;
attr R is funny means
ex T being TopRelStr st R = T;
end;

37
:LFD:

(TopRelStr is dis ussed in Se tion 5.5.1.) The argument R is used improperly in the de niens. Instead of only examining its elds, we try to
say something about R in its entirety. This abuse renders proving thefollowing laim impossible
theorem FALSE:
for R, T being RelStr st the RelStr of R = the RelStr of T & R is funnyholds T is funny;

There is no way we an su eed be ause of the following ounterexample
re onsider IR = {} as Relation of {} by RELSET_1:25;
set R = RelStr(# {}, IR #);onsider TL being empty Subset-Family of {};set T = TopRelStr(# {}, IR, TL #);T is funny by LFD;
then R is funny by FALSE;

where we have onstru ted two obje ts R and T whi h satisfy premisesof the theorem yet the on lusion is false.
Let us note that in the present implementation of Mizar we annot prove the negation of the laim named FALSE. Currently, there isonsiderable dis ussion in the Mizar proje t about an implementation of onstru tors with arguments that are stru tures whi h would
allow similar properties to be dis overed automati ally by the pro essor
when they hold. As of now, we have to prove sequen es of theorems,
sometimes long, similar to WAYBEL 8:17 above.
Another not very pleasant aspe t of the Mizar system, also on erning stru tures, is that we annot de ne a general notion of an isomorphism between stru tures. Su h a de nition is possible for stru turesde ned within a universal algebra, but there is no way to introdu e
the general notion of an isomorphism for stru tures o urring at thelanguage level.
5.5. Putting together order and topology
5.5.1. Latti es with topology
Topologies on posets indu ed by their ordering and, onversely, partial orders on topologi al spa es generated by their topologies are ofentral importan e to the theory of ontinuous latti es. Examples of

02jar.tex; 25/05/2002; 14:42; p.37

38
G. Ban erek and P. Rudni ki
su h topologies are: the S ott topology, introdu ed in the l-book
as the family of sets whi h are ina essible by dire ted sups; the lower
topology, generated by omplements of prin ipal lters as subbasi open
sets; and the Lawson topology, the ommon re nement of both.
When investigating su h topologies, we need to address the matterfrom two perspe tives simultaneously: the algebrai (latti e) perspe tive and the topologi al spa es perspe tive. In the ase of the Lawson
topology, we have to deal with three topologies and a poset at thesame time. The solution from the l-book introdu es new notations
like S ott open, S ott losed, S ott neighborhood, et . Although, it ispossible to do the same in Mizar, su h types of notations whi h are
not onsistently used in the l-book, would unne essarily ompli ate
the use of general topology notions already developed in mml andrequire many new attributes. The problem was solved by employing
multi-pre xed stru tures.
The root stru ture for topologi al spa es given in PRE TOPC [41℄ isdefinition
stru t (1-sorted)
TopStru t (# arrier -> set,
topology -> Subset-Family of theend;arrier #);and a relation is added to it in WAYBEL 9 [34℄ to obtainstru t (TopStru t, RelStr)
TopRelStr (# arrier -> set,
InternalRel -> (Relation of the arrier),
topology -> Subset-Family of the arrier #);An auxiliary mode de ned in YELLOW 9 [11℄ aptures the fa t that a
topology was added to a relational stru turedefinition
let R be RelStr;
mode TopAugmentation of R -> TopRelStr means
the RelStr of it = the RelStr of R;
end;:: YELLOW_9:def 4

The stru ture TopRelStr is both the stru ture TopStru t and the stru ture RelStr, so to an obje t of type TopRelStr one an apply attributesde ned for posets as well as attributes de ned for topologi al spa es.
If X is a TopRelStr, then we also have the following equality
the RelStr of X = RelStr(# thearrier of X, the InternalRel of X #)and a similar one holds for TopStru t. The stru ture TopRelStr provides
the \building blo ks" for introdu ing a mode of latti es with topology
in WAYBEL 9 [34℄02jar.tex; 25/05/2002; 14:42; p.38

Continuous Latti es in

Mizar

39

definitionmode TopLatti e is with_suprema with_infima reflexive transitive
antisymmetri TopSpa e-like TopRelStr;
end;

Note that TopLatti e is a more general notion than a topologi al latti e
sin e the ontinuity of meet and join operators is not required.
The attribute open is de ned for subsets of TopStr as
definition let T be TopStru t, P be Subset of T;
attr P is open means
P in the topology of T;
end;:: PRE_TOPC:def 5

and is appli able to a subset of any stru tural type widening to TopStr.
The S ott topology is a topologi al spa e having the following property
definition let T be reflexive non empty TopRelStr;
attr T is S ott means:: WAYBEL11:def 4
for S being Subset of T holds S is open iff S is ina essible upper;end;

In order to say that a subset of the arrier of TopRelStr is S ott open, we
use the attribute open together with the attribute S ott and similarly
for Lawson open (see Se tion 5.8).
As an example of this approa h, let us look at Proposition 1.6 from[25, p. 144℄.
1.6. Proposition. Let L be a omplete latti e.
(i) An upper set U is Lawson open i it is S ott open;(ii) A lower set is Lawson- losed i it is losed under sups ofdire ted sets.

The orresponding Mizar theorems appear in WAYBEL19 [12℄.
The Mizar formalization of the if ase of (i) was also formulated ina di erent way sin e every S ott open set is also upper by de nition, andthus we have two theorems for (i) shown below, and only one theoremfor (ii).
theoremfor S being S ott omplete TopLatti e,
T being Lawson orre t 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;:: WAYBEL19:37

theorem :: 1.6. PROPOSITION (i), p. 144:: WAYBEL19:41

02jar.tex; 25/05/2002; 14:42; p.39

40

G. Ban erek and P. Rudni ki

for S being S ott omplete TopLatti e,
T being Lawson orre t 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 ( omplete TopLatti e), A being lower Subset of T
holds A is losed iff A is losed_under_dire ted_sups;

5.5.2. Produ ts
Produ ts of latti es augmented with a topology are treated by separating the relational produ t from the topologi al produ t. The produ t
of a family of sets and the produ t of a family of relational stru tures
were dis ussed in Se tion 4.5. The produ t of a family of topologi al
spa es is de ned in WAYBEL18 [27℄ asdefinition let I be set,
J be TopSpa e-yielding non-Empty ManySortedSet of I;
fun produ t J -> stri t TopSpa e means:: WAYBEL18:def 3
the arrier of it = produ t Carrier J &produ t_prebasis J is prebasis of it;
end;

and we will not venture into the details of the de niens.
Item 3.4 from [25, p. 122℄ uses both produ ts, the algebrai and the
topologi al.
3.4. Lemma. (i) For every set M we have (2 ) = (2) ; thatis the S ott topology on 2 and the produ t topology agree. ...
This fa t is formalized as follows
M

M

M

theorem:: WAYBEL18:16
for I being non empty set,
T being S ott TopAugmentation of produ t (I --> BoolePoset 1)
holds
the topology of T = the topology of produ t (I --> Sierpinski_Spa e);

where BoolePoset 1 is a RelStr with arrier equal to 2 ordered byin lusion. Therefore I --> BoolePoset 1 is RelStr-yielding and the
produ t of the latter is the relational produ t as mentioned on p. 19.
Sierpinski_Spa e is a topologi al spa e equal to TopStru t(# 2, 3 #)de ned askdefinition
fun Sierpinski_Spa e -> stri t TopStru t means
the arrier of it = {0,1} &the topology of it = {{}, {1}, {0,1} };end;:: WAYBEL18:def 9

02jar.tex; 25/05/2002; 14:42; p.40

Continuous Latti es in

Mizar

41

Hen e, an indexed set of su h spa es I --> Sierpinski_Spa e is TopSpa eyielding and its produ t is the topologi al produ t mentioned above.
This overloading of produ t is very onvenient but also potentiallytroublesome; namely, if M is a ManySortedSet and M has both the RelStrand TopSpa e-yielding attributes, then there is a question of whether
produ t M is the relational produ t or the topologi al produ t? Currently
in Mizar the answer depends on the ontext whi h is ontrolled by the
text author. However, there is no way to dire tly say whi h produ t
is meant and this situation is not satisfa tory. The way around the
problem is to de ne synonyms for both produ ts that will distinguishthem notationally, see WAYBEL26 [15℄.
definition
let I be set, J be RelStr-yielding ManySortedSet of I;
redefine fun produ t J;
synonym I-POS_prod J;
end;definition
let I be set, J be TopSpa e-yielding non-Empty ManySortedSet of I;
redefine fun produ t J;
synonym I-TOP_prod J;
end;

5.6. Alexander's lemma
Alexander's lemma is a riterion for topologi al ompa tness in termsof overs and subbases. In [32, p. 139℄, it is presented as
6 Theorem (Alexander) If S is a subbase for the topology of a
spa e X su h that every over of X by members of S has a nite
sub over, then X is ompa t.

The way below relation, written as  in the l-book, may be seen
as a generalization of a on ept related to topologi al ompa tness.
It is derived from the on ept of U is relatively ompa t in V , foropen sets U and V (U is ompa t if U is relatively ompa t in itself).
This was explored in WAYBEL 3 [7℄ to show the orresponden e between
lo ally ompa t topologi al spa es and ontinuous latti es. The orresponden e between way below and topologi al openness and sub overs
is expressed by the following lemmas
theoremfor T being non empty TopSpa e,
x, y being Element of In lPoset the topology of T
st x is_way_below y:: WAYBEL_3:34

02jar.tex; 25/05/2002; 14:42; p.41

42

G. Ban erek and P. Rudni ki

for F being Subset-Family of the arrier of T
st F is open & y = union F
ex G being finite Subset of F st x = union G;
theorem:: WAYBEL_3:35
for T being non empty TopSpa e,
x, y being Element of In lPoset the topology of T
st for F being Subset-Family of T st F is open & y = union F
ex G being finite Subset of F st x = union G
holds x is_way_below y;With the following de nition
definition :: CCL 1.1, p. 38
let L be non empty reflexive RelStr, x be Element of L;
attr x is ompa t means:: WAYBEL_3:def 2
x is_way_below x;
synonym x is isolated_from_below;
end;

we an state the main lemmas of interest
theoremfor T being non empty TopSpa e,
x being Element of In lPoset the topology of T,
X being Subset of T st x = X
holds x is ompa t iff X is ompa t;:: WAYBEL_3:36

theoremfor T being non empty TopSpa e,
x being Element of In lPoset the topology of T
st x = the arrier of T
holds x is ompa t iff T is ompa t;:: WAYBEL_3:37

The ompa t attribute on the left-hand side is de ned by WAYBEL 3:def
2 and on the right-hand side it means ompa t in the topologi al sense.

Pursuing this orresponden e, a generalization of Alexander's lemma
is given in [25, Ch. I, p. 74℄
3.21. Proposition. Let B be a olle tion of open subsets forminga subbase for the topology of a spa e X , and let U and V be open
sets with U  V . Then a ne essary and suÆ ient ondition for
U  V is that every over of V by members of B has a nite
sub over of U .

This generalization was formalized in WAYBEL 7 [9℄theorem:: WAYBEL_7:35
for T being non empty TopSpa e, B being prebasis of Tx, y being Element of In lPoset the topology of T

02jar.tex; 25/05/2002; 14:42; p.42

Continuous Latti es in

st x

Mizar

43

= y holds x << yiff
for F being Subset of B st y = union F
ex G being finite Subset of F st x = union G;

The mode prebasis of orresponds to the ommonly used term of a
subbase. Note, that the meaning of sub over is stated expli itly. Fortunately, we did not have to de ne the mode prebasis as it alreadyexisted in mml in CANTOR 1 [47℄definition
let X be TopStru t;
mode prebasis of X -> Subset-Family of X means
it = the topology of X &ex F being Basis of X st F = FinMeetCl it;
end;:: CANTOR_1:def 5

where Basis of X is
definition
let X be TopStru t;
mode Basis of X -> Subset-Family of X means
it = the topology of X & the topology of X:: CANTOR_1:def 2= UniCl it;

Here, UniCl and FinMeetCl of a family of sets are losures under arbitrary unions and under nite interse tions, respe tively.
We thought we were less fortunate with the on ept of sub oversin e there was no orresponding de nition for it in mml. The author
formalizing theorem WAYBEL 7:35 struggled with the idea of de ning a
new mode (type onstru tor) for sub over of. This mode would taketwo arguments: a set and a family of sets. However, it turned out thatin this parti ular theorem [25, Ch. I, 3.21℄, the term sub over is not
used in a straightforward way: we have U  V , B is a over of V ,and we want to say that there exists a sub over of U hosen from B.
Of ourse B is also a over of U as U  V . An attempt to expressin Mizar all the needed type dependen ies required new notions. It
also required a revision of mml as the notion of a over was de ned
in COMPTS 1 for types too narrow for our needs. Instead of doing all
this, the meaning of sub over was expressed dire tly in the theorem.
The meaning of sub over is expressed very su in tly as it uses only
the predi ate = and the fun tor union. Note that this takes the same
number of hara ters as typing sub over! Issues like this seem to be
insigni ant yet they onsume quite some time when one tries to beformal.
The Mizar proof of Proposition 3.21 in [25, Ch. I℄ is about 8 times
longer than the proof from the l-book (if we ount words) but thereasoning is almost the same. In a Mizar proof we must refer expli itly

02jar.tex; 25/05/2002; 14:42; p.43

44
G. Ban erek and P. Rudni ki
to all premises and inferen e steps are more detailed sin e in most ases
the Mizar he ker is not as bright as most human readers.
In formal texts we have to provide an expli it analysis of all degenerate ases: empty, trivial, non proper, et . This is one of the more signi ant di eren es between formal proofs and proofs in the l-book.
Su h analyses revealed some gaps in the l-book.
The Mizar proof of Alexander's lemma in WAYBEL 7 [9℄ uses thefollowing fa tjtheorem:: WAYBEL_7:30
for L being non trivial Boolean LATTICE, F being proper Filter of L
ex G being Filter of L st F = G & G is ultra;

whi h for ed us to analyze some aspe ts of non trivial latti es. In mml,
the attribute trivial has several meanings, depending on the type ofthe obje t to whi h it is applied, but the one relevant here on erns
stru tures derived from 1-sorted and is de ned in [16℄definition let X be set;
attr X is trivial means
X is empty or ex x being set st X = {x};end;definition let S be 1-sorted;
attr S is trivial means
the arrier of S is trivial;end;:: REALSET1:def 12:: REALSET1:def 13

A stru ture that is non trivial has at least 2 elements in its arrier.
Stru tures that are trivial have many uses sin e a trivial (but non
empty) RelStr is the simplest obje t serving as a model for any latti eequality. This is used in proving orre tness of existential registrations .
In 68 existential registrations of di erent kinds of latti es in the YELLOW
and WAYBEL series, there are 21 that use trivial RelStr as an example
of existen e and only 5 whi h employ non trivial ones (the remaining
ones do not mention the adje tive). There are also 18 onditional registrations stating that trivial implies some latti e properties and only
1 uses the non trivial ase. It turns out that trivial things have quite
non trivial uses!
i5.7. The S ott topology
One of the obje tives of the theory of ontinuous latti es is a hara terization of the orresponden e between latti e theoreti notions andtopologi al notions. The starting point for the algebrai side is thenotion of lim-inf onvergen e formalized in WAYBEL11 [53℄ as

02jar.tex; 25/05/2002; 14:42; p.44

Continuous Latti es in

Mizar

45

definition let R be non empty RelStr, N be net of R;
fun lim_inf N -> Element of R equals:: WAYBEL11:def 6"\/" ( { "/\"( { N.i : i >= j }, R )where j is Element of the arrier of N: not ontradi tion}, R );
end;

where "/\"(X,R) is the in mum and "\/"(X,R) is the supremum of X wrt
onstru t S ott's topology.
First, we de ne the S ott onvergen e lassR, respe tively. Now, one is in a position todefinition let R be reflexive non empty RelStr;
fun S ott-Convergen e R-> Convergen e-Class of R means :: WAYBEL11:def 8
for N being stri t net of R st N in NetUniv R
for p being Element of the arrier of R
holds [N, p℄ in it iff p <= lim_inf N;
end;

A TopRelStr is S ott a ording to de nition WAYBEL11:def 4 quoted in
Se tion 5.5.1 where open sets are hara terized in latti e terms. One
now proves the key theorem:
theorem:: WAYBEL11:32
for T being omplete S ott TopLatti eholds the TopStru t of T = Convergen eSpa e S ott-Convergen e T;

( f. Se tion 4.6). In addition, for every omplete and ontinuous LATTICE,
its S ott-Convergen e is topologi al, i.e., it satis es the onditions statedin Figure 1. In order to follow the l-book, we also de ned a separate
fun tor denoting the S ott topology
definition let L be non empty reflexive RelStr;
fun sigma L -> Subset-Family of L equals:: WAYBEL11:def 12
the topology of Convergen eSpa e S ott-Convergen e L;
end;

The formalization of S ott's topology was nished in WAYBEL14 [21℄.
In the proof of
1.15. Corollary. For any omplete latti e L the following onditions are equivalent(1) L is algebrai .
(2) The S ott topology has a basis of sets " k where k 2 K (L)(3) (L) is algebrai and has enough o-primes.

from [25, p. 108℄, a simpli ation was found. Typi ally, theorems ofthis form are proven as a sequen e of impli ations, say (1) ) (2),02jar.tex; 25/05/2002; 14:42; p.45

46
G. Ban erek and P. Rudni ki(2) ) (3) and (3) ) (1), and this is indeed what is done in the lbook. While formalizing the last impli ation, we ould not follow one of
the given hints and thus we ompleted the proof by proving (3) ) (2)and then (2) ) (1). The proof in the book turned out to be orre t,
but we ended up with a simpler proof. A small reward for all theseformalization hores!
5.8. The Lawson topology
The Lawson topology is formalized in WAYBEL19 [12℄ as a re nement of
S ott's topology and the so alled lower topology. The latter is de ned
asdefinition :: 1.1. DEFINITION, p. 142 (part I)
let T be non empty TopRelStr;
attr T is lower means:: WAYBEL19:def 1{ -uparrow x where x is Element of T: not ontradi tion }is prebasis of T;
end;

The Lawson topology is then de ned as
definition :: 1.5. DEFINITION, p. 144 (part I)
let T be reflexive (non empty TopRelStr);
attr T is Lawson means(omega T) \/ (sigma T) is prebasis of T;
end;:: WAYBEL19:def 3

where omega T is the lower topology and sigma T is the S ott topology. The formalization of the material on Lawson's topology has notbeen ompleted; of 55 items, 17 are still not done and the material
in these remaining items be omes more and more advan ed. Arti le
WAYBEL21 [13℄ an serve as a ase in point of the volume of preparatory
material needed to prove the more advan ed items.
Arti le WAYBEL21 formalizes two items from the l-book, Theorem
1.8 from p. 145 and Theorem 1.11 from pp. 146{147. Both theorems
state the equivalen e of three statements, thus their proofs onsist ofjustifying sequen es of impli ations. The entire arti le is 2,130 lines longand the a tual proofs of theorems take only 400 lines. But 1600 lines
were needed to develop some auxiliary, frequently very te hni al, fa ts
su h as: properties of semi-latti es and morphisms of SubRelStrs. These
properties probably also have potential for reuse, but really belong to
the YELLOW series. The remaining 100 lines on ern a generalization ofLemma 1.7 from [25, p. 145℄
Let L be a omplete latti e and F a ltered subset.
Then inf F = lim F with respe t to (L), and this limit is unique.

1.7. Lemma.

02jar.tex; 25/05/2002; 14:42; p.46

Mizar47((L) is the Lawson topology for L). A formalization of this lemma, by
the same author, originally appeared in WAYBEL19 [12℄ asContinuous Latti es intheoremfor T being Lawson ( omplete TopLatti e),
F being non empty filtered Subset of T
holds Lim (F opp+id) = {inf F};:: WAYBEL19:43

and then its revised version was put into WAYBEL21 [13℄theorem:: WAYBEL21:44:: 1.7. LEMMA, -- WAYBEL19:43 revisedfor T being Lawson ( omplete TopLatti e)
N being eventually-filtered net of T
holds Lim N = {inf N};

Without going into the details of both formulations of the lemma, we
simply note that we frequently fa ed similar situations in whi h it was
un lear whether we should keep one version of the theorem, or theother, or both. If we kept only one then would it be in the original arti leor the new one? Depending on the answer to this question, revisions ofpast work be ame ne essary and tools automating the pro ess of su hrevisions are being onsidered. The frequen y of su h ases prompted
more dis ussion about a long pending redesign of the organization ofmml (see Se tion 4.3).
h5.9. Duality theory
Duality of latti es is a meta-property, that is a property of the theory oflatti es. The simplest duality of latti es roughly says that any theorem
formulated in terms of inf, sup, > and ? remains true if we repla ethem by sup, inf, ? and >, respe tively. This type of duality is overed
in YELLOW 7 [8℄. The l-book overs more ompli ated dualities, forexample, the dualities of inf- and sup-preserving maps in the framework of Galois onne tions. In essen e, these dualities an be expressed
entirely within the latti e theoreti framework. While ategory theory
helps us in formulating the gist of duality, it is of little use in obtaining
dual theorems dire tly.
The rst idea of how to formalize duality in the l proje t was
to apture it without using ategory theory, but we knew this would
result in greatly in reasing the number of de nitions and theorems.
The de nitions would be for fun tors expressing duality by transforming latti es and maps between them. The respe tive theorems would
present the essen e of duality without engaging ategory theory. Thisapproa h seemed quite appealing and reasonable sin e we ould not
spot a pla e in the l-book where ategory theory is used ex ept

02jar.tex; 25/05/2002; 14:42; p.47

48
G. Ban erek and P. Rudni ki
for the su in t formulation of ertain meta-properties of latti es. In
pra ti e, the latti e formulation of properties behind duality has morevalue. Another aspe t of this approa h's appeal was that mml did not
ontain a formalization of ategory theory in a form onvenient for the
l proje t.
However, formulating duality of latti es in the language of ategory
theory seemed like an important test for the formal hara terization ofduality on epts. Besides, the l-book uses the language of ategory
theory and we wanted to follow the book losely.
The work of formalizing duality theory has just started and at the
moment the related arti les ontain formulations in both the latti enomen lature and the language of ategories. As an example, let us
onsider the following from the l-book, p. 179.
1.3. Theorem. (INF-SUP duality). The ategories INF and
SUP are dual under the fun tors D and G given by the Galois
onne tion of fun tions. Spe i ally, D and G preserve obje ts (theis, the \dual" of a omplete latti e is itself under this duality).
Moreover GD(g) = g and DG(d) = d for all g in INF and all din SUP.

The two ategories of interest are de ned as
1.1. De nition The ategories INF and SUP have the samelass of obje ts, namely, the lass of all omplete latti es. The
morphisms of INF preserve arbitrary infs, the morphisms of SUP
preserve arbitrary sups.
Without using the terminology of ategory theory, the above theorem
an be formalized astheorem:: WAYBEL34:10 :: 1.3. THEOREM, p. 179
for S, T being omplete LATTICE, g being infs-preserving map of S, T
holds UpperAdj LowerAdj g = g;theorem:: WAYBEL34:11 :: 1.3. THEOREM, p. 179
for S, T being omplete LATTICE, d being sups-preserving map of S, T
holds LowerAdj UpperAdj d = d;where the LowerAdj is de ned as
definition
let S, T be LATTICE, g be map of S, T;
assume S is omplete & T is omplete & g is infs-preserving;
fun LowerAdj g -> map of T,S means:: WAYBEL34:def 1[g, it℄ is Galois;
end;

02jar.tex; 25/05/2002; 14:42; p.48

Continuous Latti es in

Mizar

49

The UpperAdj is de ned analogously.
When using the terminology of ategories for expressing the samefa ts, we run into the foremost problem, mentioned in Se tion 4.7.
Namely, in mml we annot have a ategory of all ontinuous latti es as
we must deal only with sets. Therefore, one of the ategories of interest
is de ned as
definition :: 1.1 DEFINITION, p. 179
let W be non empty set; given w being Element of W su h thatw is non empty;
fun W-INF_ ategory -> latti e-wise stri t ategory means:: WAYBEL34:def 4(for x being LATTICE holds x is obje t of it
iff x is stri t omplete & the arrier of x in W) &for a,b being obje t of it, f being monotone map of latt a, latt b
holds f in <^a, b^> iff f is infs-preserving;end;

and the de nition of the other is analogous. The restri tion to a set W
serving as the sour e of arriers for our ategories is not that importantas the set an be as large as our set theory permits. Note that theassumption of W ontaining at least one non empty set is purely te hni al
as it eliminates just one set, namely 1, see Endnote k.
With these ategories de ned, we an now formulate duality in thelanguage of ategories.
theorem:: WAYBEL34:19 :: 1.3 THEOREM, p. 179
for W being with_non-empty_element set holds(W LowerAdj)*(W UpperAdj) = id (W-SUP_ ategory) &(W UpperAdj)*(W LowerAdj) = id (W-INF_ ategory);
theorem:: WAYBEL34:20 :: 1.3 THEOREM, p. 179
for W being with_non-empty_element set holds
W-INF_ ategory, W-SUP_ ategory are_anti-isomorphi ;where the types of W LowerAdj and W UpperAdj are
ontravariant Fun tor of W-INF_ ategory, W-SUP_ ategory
ontravariant Fun tor of W-SUP_ ategory, W-INF_ ategory

respe tively. Their de nitions are te hni ally ompli ated and we do
not quote them here.
Fortunately, the basi on epts of ategory theory needed to formulate the above theorem were already available in FUNCTOR0 [51℄definition let A,B be transitive with_units (non empty AltCatStr);
pred A,B are_anti-isomorphi means:: FUNCTOR0:def 41
ex F being Fun tor of A,B st F is bije tive ontravariant;symmetry;end;

02jar.tex; 25/05/2002; 14:42; p.49

50
G. Ban erek and P. Rudni ki
We will not go into the details of the de niens: the terms used there
orrespond to the ommon terminology of ategory theory. Here wewould like to stress again the importan e of systemati ally developing
a data base of formalized mathemati s like mml. The basi s of ategory
theory were in luded in mml long before they were needed for the lproje t.
6. The length of formal texts, osts

Probably the most interesting statisti s would be the lengths of formal
texts reated in this proje t ompared to the original l-book. Thesegures an be used to ompute the so alled the de Bruijn fa tor, but
we run into some diÆ ulties in de iding whi h measure to use.
Table II. The de Bruijn fa tors
MeasureChara ters (bytes)
Compressed
Lines
Tokens (words)

Thel-book Formalized The de Bruijn fa tor
312,620

 90 000;

4,466
66,9903,098,460
566,720
82,749808,020

9.91
6.29
18.52
12.06

The items formalized thus far o upy 111.65 pages in the l-book.
This material is formalized not only in the WAYBEL series but also in someother mml arti les that were revised for the purpose of the l proje t.
We in lude these other arti les in our omparisons so the numbers here
di er slightly from the ones given in Se tion 7. We believe that thesenumbers tell something but the reader should be aware that a lot ofmaterial in the WAYBEL series should have been lo ated in the YELLOW
series or other mml arti les. Some lean up is de nitely due.
For this omparison, we assumed that the l-book has 40 lines
per page, 70 hara ters per line and 15 tokens per line. These assumptions are on the onservative side as we were too lazy to do the exa tounting and we do not have the l-book available in ele troni form.
Table II presents the numbers. Note that the formalization o upies
only 566,720 bytes when ompressed so the text is quite redundant;
unfortunately, we annot o er the orresponding number for the lbook. However, it is believed that material like the l-book be omes
somewhere between 3 and 4 times shorter when ompressed. Thus, inthis table we used a ompression rate of 3.5.

02jar.tex; 25/05/2002; 14:42; p.50

Mizar51
F. Wiedijk [60℄ reported some omparisons of de Bruijn fa tors fordi erent types of mathemati al texts and he used WAYBEL14 [21℄, whi hformalizes pages 105{108 of the l-book, as one of the ases. He used
only the byte ount and obtained the results shown in Table III.
Continuous Latti es inTable III. The de Bruijn fa tor(s) for WAYBEL14 from [60℄informal formal de Bruijn fa tor
un ompressed
11.7 K 78.4 K
apparent 6.7
ompressed
4.0 K 16.3 K
intrinsi 4.1

We annot o er any reliable or even substantiated laims about theost of the l proje t measured in man-years. F. Wiedijk [59℄ ame
to the on lusion that writing a Mizar arti le takes approximately
1 month of work, and 1.5 months if we take into a ount the maintenan e of mml. Applying these numbers on 57 arti les in the lproje t results in somewhere between 5 and 7.5 man-years. Sin e nore ords of this type have been kept for the proje t, it is hard to say
how a urate these numbers are. We have the impression that they
are an underestimate|many arti les took substantially longer than amonth to omplete while several were written in about a week. Many
hours of e ort of a general nature, espe ially on the part of the proje tleader G. Ban erek, not asso iated with any parti ular arti le are hardto put in numbers. Also, for many parti ipants of the proje t a substantial amount of time was needed to learn the material they were
supposed to formalize, and again it is hard to do a ounting of su htime. Certainly, this time varied signi antly among the authors andthere was a generally shared impression that the material in the WAYBEL
series needed mu h more work per line than in the YELLOW series (butsome of the YELLOW arti les posed essential hallenges). This impression
be omes more apparent with the later items of the l-book.
7. Some other statisti s

The l proje t started in 1996. The l-book ontains 334 pages
divided into 8 hapters overing a total of 715 items. Of these, 254
items are examples and exer ises whi h we did not plan to over. By
the end of April 2002, the formalization overed 231 items whi h isslightly more than 50% of the work originally planned. (A aveat isin pla e: items di er substantially in their weights and many of theremaining items seem to be more diÆ ult to formalize as their proofs
are diagram based.)

02jar.tex; 25/05/2002; 14:42; p.51

52

G. Ban erek and P. Rudni ki

Table IV.

l arti les over the years

year

1996

1997

1998

1999

2000

2001

Total

YELLOW
WAYBEL
All

8
10
18

1
6
7

5
8
13

3
4
7

1
5
6

4
2
6

22
35
57

Table V. Some arti le statisti s

mml WAYBEL YELLOW W and Y Per entage
Arti lesTheorems
Average
Min
MedianMax

717
31,741
44.3
0
37
194

35
1,512
43.2
18
41
90

22
1,018
46.3
14
49
72

57
2,530
44.4
14
43
90

7.95%
7.97%

De nitions
Average
Min
Median
Max

6,093
8.5
0
6
49

271
7.7
0
5
40

138
6.3
0
5
26

409
7.2
0
5
40

6.7%

Tokens (,000)
Average
Min
MedianMax

16,21922,58950
18,704
248,314787
22,49810699
22,04533,217471
21,431
8,762
17,62255,5671259
22,086
8,762
20,591
55,5677.76%

Size (kB)
Average
Min
MedianMax

52,184
72.8
0.9
62.2
640.0

3,027
86.5
41.1
86.5
121.4

1,671
75.9
29.9
66.9
166.3

4,699
82.4
29.9
77.4
166.3

9%

Table IV summarizes the number of arti les submitted to mml fromthis proje t. The YELLOW series onstitutes 38.6% of the arti les, mu hless than originally anti ipated. However, this may hange in the near
future as we are approa hing the part of the l-book whi h is poorly
overed in mml.

02jar.tex; 25/05/2002; 14:42; p.52

Continuous Latti es in

Mizar

53

Table VI. External referen es
External referen es

mml % W&Y

Count

Avg Min Med Max
over relevant arti les%

Out W&Y to W&Y
Out W&Y to out W&Y

371,795
13,168859
340,791

518.5
18.4
1.3
516.4

0
0
0
0

392
0
0
380

6,024
1,017
149
6,024

100.00
3.54
0.23
91.66

W&Y toW&Y to W&Y
W&Y to out W&Y

30,14512,30917,836

528.9
215.9
312.9

143
0
39

476
201
266

2,076
1,017
1,059

8.11
3.31
4.80

mml
mml to W&Y
mml

100
40.83
59.17

Table V presents the size of the proje t in terms of theorems, definitions, and sheer bytes. The last olumn is the per entage of thisproje t's ontribution to the entire mml. Average numbers of theorems,de nitions, tokens, and kilobytes show that arti les in the proje t arelose to the mml average. Note the smaller average number of de nitions whi h may indi ate that the theory is explored more intensively.
The intera tion between the l proje t and the rest of the mml,
may be measured by the number of referen es between the proje tarti les and other mml arti les as presented in Table VI. The per entage
of all external referen es from the YELLOW and WAYBEL arti les to therest of mml is 59.17%. This indi ates that mml ontained a substantial
quantity of de nitions and fa ts needed for our proje t.
8. Con lusions

Our general on lusions are that the Mizar system seems satisfa tory
for formalizing advan ed mathemati s and that mml was a satisfa torily ri h base for starting the formalization of the l-book. Let us
now look at the answers to the questions that were posed for the lproje t as stated in Se tion 2.
The expressive power of the Mizar language is suÆ ient for formulating the de nitions, theorems, and proofs ontained in thel-book.
The ontents of mml were reused to a substantial degree with somerevisions.

02jar.tex; 25/05/2002; 14:42; p.53

54

G. Ban erek and P. Rudni ki

Di erent on epts introdu ed in independent arti les ould be used
together quite smoothly.
The Mizar software handled the large amounts of material withno problems after adjusting some quantitative parameters.
Unfortunately, almost no re ords were kept that would provide
reliable data about the human e ort required for this proje t.
Formalization in Mizar is still not as onvenient as doing mathemati s traditionally, but the system is being ontinually improved. Even
now, there are some obvious gains from formalizing mathemati s in
Mizar: the results are me hani ally he ked, the stored knowledge an
be browsed ele troni ally, and most importantly all the on epts|nomatter how small or simple|must be expli itly stated. These fa tors
provided substantial help for Mizar authors, espe ially to the newparti ipants in the proje t. The ma hine stored information may be mehani ally explored, hanged, generalized, and edited. Reorganizationof ma hine readable mathemati al texts is mu h easier than reorganization of su h texts written informally and su h reorganizations were
performed frequently in our proje t.
The work done in this proje t resulted in numerous improvementsof the Mizar system and revealed a number of issues whi h are now
being investigated further:
The urrent organization of the data base as a loose olle tion ofarti les is not very onvenient and it is headed for serious problems
when the data base be omes larger, say by an order of magnitude.
It seems that the library should be based on units having monographi al nature as the urrent organization of mml leads to thefragmentation of related information.
h

We need tools for sear hing mml, whi h are better than just textual
sear hes used now. In parti ular, we need tools for stati syntax
based sear hing whi h an distinguish homonyms, identify synonyms, and take into a ount hidden arguments of onstru tors,
while eliminating the dependen e on identi ers.
The Mizar veri er, the heart of this proof assistant, should be furnished with some apabilities for automati algebrai manipulationby employing te hniques from omputer algebra.
Sin e frequent revisions of mml seem inevitable, there is a needfor an automated me hanism whi h will support this pro ess.

02jar.tex; 25/05/2002; 14:42; p.54

Mizar55
By fo using improvements to the Mizar language and its implementation toward:
 the development of a ri her syntax for the formulation oftheorems, de nitions and proofs,
 strengthening of the inferen e he ker to shorten proofs,
 in reased exibility in the type system, the addition of attributes with expli it arguments,
 a more onvenient semanti s of stru ture types
we an derive great bene ts for the development of mml-like repositories.
We would like to end with the following question: who will nan ially
support the development of a sizable data base of formal mathemati s?
At the moment, nishing the l-proje t depends on the answer.
Continuous Latti es in

A knowledgements

We would like to express our gratitude to Professors Y. Nakamura andY. Shidama for reating a very pleasant environment for us in Nagano
while we were working on this report. We would like to thank Pauline N.
Kawamoto for polishing the English of this text as our original writing
seemed to be too Polish even to us.
Notes
a

Mizar

might be onsidered as an Esperanto for mathemati s and there aresome similarities between the two languages. Esperanto was developed in Bialystok
by Ludwik Zamenho and the development ofis also based in Bialystok.
Esperanto is an arti ial international language with words taken from several national languages and uses a quite regular grammar.
may be onsidered as an
attempt to standardize the language of mathemati s. There are many translationsof books into Esperanto and it is possible to learn the language by reading thesetranslations. There is a large olle tion of
texts and we know several people
who learned
by reading them.
b Other areas in whi hhas been developed in a fo used way are: Jordan'surve theorem, formal treatment of omputations and ir uits, real and omplex
analysis, and algebra for symboli omputations.
Ea harti le has, besides a regular title, an identi er whi h is used whenreferring to it. Be ause of the DOS prehistory of the proje t, the names ofarti les are limited to 8 hara ters and use the .MIZ extension.

Mizar
Mizar

Mizar

Mizar

mml

Mizar

Mizar

02jar.tex; 25/05/2002; 14:42; p.55

56

G. Ban erek and P. Rudni kildOver the years, the work on formalizing the-book has been supported partially by grants from: ONR N00014-95-1-1336 and N00014-97-1-0777 (USA), KBN
8 T11C 018 12 (Poland), NSERC OGP 9207 (Canada), NATO CRG 951368, JSPS
P00025 (Japan) and Shinshu Endowment Fund for Information S ien e (Nagano,
Japan).
e Clusters are used to express the following relationships:
Conditional registrations are used to say that obje ts having a property expressedby some attributes also have another property expressed by other attributes.
For example,
luster non trivial -> non empty set;says that every non trivial set is non empty. We have to prove that it isindeed the ase.
Term adje tive registrations say that a term onstru ted with a spe i fun tor g
has a ertain property expressed by attributes. For example, if A is a poset
then we may haveluster the InternalRel of A -> Order-like;whi h we have to prove. These registrations are frequently alled fun torial
registrations although they are appli able to terms.

Existential registrations are used to de ne new type expressions that involve attributes. For example,
luster non empty reflexive transitive antisymmetri

stri t RelStr;

Mizar

and it requires a proof of existen e of su h an obje t as
types are non
empty.
The relationships expressed by lusters are automati ally pro essed by the
pro essor.
f Attribute stri t is built-in. It means that a stru ture branded stri t has
only the elds of the named stru ture and in parti ular is not derived from thisstru ture by adding other elds. Thus, a stri t RelStr has only two elds:
arrier and InternalRel.
g Fun tors are onstru tors of terms. We borrowed the name \fun tor" from [42,p. 148℄:... some signs in the formalized language should orrespond to the mappings andfun tions being examined. These signs are alled fun tors, or|more pre isely|
m-argument fun tors provided they orrespond to m-argument mappings fromobje ts to obje ts (m = 1, 2, ...).
The de nition of a fun tor in ludes a proof of orre tness in whi h one must demonstrate the existen e and uniqueness of the fun tor being de ned. Mizar fun tors
must not be onfused with fun tors as used in ategory theory.
h Re ently, theteam has started a proje t to reorganizeand put it
into{ En y lopedia of Mathemati s in.
will still onsist of arti les,albeit monographi al in nature, andarti les will be treated as \raw" material.
At the time of this writing, only materials related to Boolean properties of sets in thespirit of the eliminated arti le BOOLE [57℄ are in luded inas arti les XBOOLE 0
and XBOOLE 1. Originally, the ontents of these arti les were spread over 17
arti les.
i Rede nitions allow for hanges in the usage of previously de ned onstru tors.
Typi al rede nitions over:

Mizar

emm

Mizar

mml

mml

Mizar emm

emm

mml

02jar.tex; 25/05/2002; 14:42; p.56

Continuous Latti es in

Mizar

57

hanges to the signature of a onstru tor, for example by narrowing the typesof some arguments;
hanges in the de niens whi h make it more onvenient yet preserve the original
meaning.
Rede nitions are heavily used in.
j Some errors found in:
In Chapter I, Remark 3.18, p. 73, in order to prove that (1) i (3), one also
needs F to be proper unless prime lters are proper whi h is not assumed intheir de nition.
In Chapter I, Proposition 3.24, p. 75, it is not true that (2) implies (3), a
ounterexample is provided in WAYBEL 7 [9℄ theorem WAYBEL 7:41.
k Natural numbers inare von Neumann ordinals and thus: 0 = fg, 1 =ffgg, 2 = f fg, ffgg g ( = bool 1), and so on.

l

mml

Mizar

A note on referen es to Mizar arti lesReferen es to Mizar arti les are given to the printed journal Formalized Mathemati s. This journal prints the versions of Mizar arti lesas originally a epted for in lusion into mml. These arti les are mehani ally translated into English and then automati ally typeset with
TEX. As mml evolves over time, the urrent versions of Mizar arti les are put into the Journal of Formalized Mathemati s (JFM) an
ele troni publi ation available at http://mizar.org/JFM. In JFM, as inmml, the name of an arti le is used as its identi er and thus we in luded
these names in the referen es below. Some mml arti les exist only in
ele troni form as they were reated as a result of mml revisions.
Referen es
1. Grzegorz Ban erek. Tarski's lasses and ranks. Formalized Mathemati s,
1(3):563{567, 1990.
: CLASSES1.
2. Grzegorz Ban erek. Konig's theorem. Formalized Mathemati s, 1(3):589{593,1990.
: CARD 3.
3. Grzegorz Ban erek. Cartesian produ t of fun tions. Formalized Mathemati s,2(4):547{552, 1991.
: FUNCT 6.
4. Grzegorz Ban erek. Complete latti es. Formalized Mathemati s, 2(5):719{725,1991.
: LATTICE3.
5. Grzegorz Ban erek. Bounds in posets and relational substru tures. Formalized
Mathemati s, 6(1):81{91, 1997.
: YELLOW 0.
6. Grzegorz Ban erek. Dire ted sets, nets, ideals, lters, and maps. Formalized
Mathemati s, 6(1):93{107, 1997.
: WAYBEL 0.
7. Grzegorz Ban erek. The \way-below" relation. Formalized Mathemati s,
6(1):169{176, 1997.
: WAYBEL 3.

mml

mml

mml

mml

mml

mml
mml

02jar.tex; 25/05/2002; 14:42; p.57

58

G. Ban erek and P. Rudni ki

8. Grzegorz Ban erek. Duality in relation stru tures. Formalized Mathemati s,
6(2):227{232, 1997.
: YELLOW 7.
9. Grzegorz Ban erek. Prime ideals and lters. Formalized Mathemati s,
6(2):241{247, 1997.
: WAYBEL 7.
10. Grzegorz Ban erek. Arithmeti of Non Negative Rational Numbers. Journalof Formalized Mathemati s, Addenda.
: ARYTM 3.
11. Grzegorz Ban erek. Bases and re nements of topologies. Formalized Mathemati s, 7(1):35{43, 1998.
: YELLOW 9.
12. Grzegorz Ban erek. The Lawson Topology. Formalized Mathemati s, 7(2):163{
168, 1998.
: WAYBEL19.
13. Grzegorz Ban erek. Lawson topology in ontinuous latti es. Formalized
Mathemati s, 7(2):177{184, 1998.
: WAYBEL21.
14. Grzegorz Ban erek. Development of the theory of ontinuous latti es in.
Symboli Computation and Automated Reasoning, M. Kerber and M. Kohlhase,
Eds., A K Peters, 2001.
15. Grzegorz Ban erek. Continuous latti es of maps between T0 spa es. Formalized
Mathemati s, 9(1):111{117, 2001.
: WAYBEL26.
16. Jozef Bialas. Group and eld de nitions. Formalized Mathemati s, 1(3):433{
439, 1990.
: REALSET1.
17. Ewa Bonarska. An Introdu tion to PC Mizar. Fondation Philippe le Hodey,
Brussels, 1990. Revised version, 2000.
http://mizar.org/proje t/bibliography.html.
18. Czeslaw Bylinski. Some basi properties of sets. Formalized Mathemati s,
1(1):47{53, 1990.
: ZFMISC 1.
19. Czeslaw Bylinski. Introdu tion to ategories and fun tors. Formalized
Mathemati s, 1(2):409{420, 1990.
: CAT 1.
20. Czeslaw Bylinski. Category Ens. Formalized Mathemati s, 2(4):527{533, 1991.
: ENS 1.
21. Czeslaw Bylinski and Piotr Rudni ki. The S ott topology. Part II. Formalized
Mathemati s, 6(3):441{446, 1997.
: WAYBEL14.
22. M. Davis. Obvious logi al inferen es. In Pro eedings of the 7th IJCAI, pages
530{531, 1981.
23. A. Degtyarev, A. Lyaletski, and M. Morokhovets. Eviden e algorithm andsequent logi al inferen e sear h. In LNAI 1705, pages 44{61, 1999.
24. H. Friedman. FOM: 107: Automated proof he king, May 2001.
www.math.psu.edu/simpson/fom/postings.
25. G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove, and
D. S. S ott. A Compendium of Continuous Latti es. Springer-Verlag, Berlin
Heidelberg New York, 1980.
26. Adam Grabowski and Robert Milewski. Boolean posets, posets under in lusionand produ ts of relational stru tures. Formalized Mathemati s, 6(1):117{121,1997.
: YELLOW 1.
27. Jaroslaw Gryko. Inje tive spa es. Formalized Mathemati s, 7(1):57{62, 1998.
: WAYBEL18.
28. Andrzej Grzegor zyk. Zarys arytmetyki teorety znej. Biblioteka Matematyzna. PWN, Warszawa, 1971.
29. Stanislaw Jaskowski. On the Rules of Supposition in Formal Logi . Studia
Logi a. Warsaw University, 1934. Reprinted in S. M Call, Polish Logi in
1920{1939, Clarendon Press, Oxford.
30. Peter T. Johnstone. Stone Spa es. Cambridge University Press, Cambridge,
London, New York, 1982.

mml
mml

mml

mml

mml

mml

mml

Mizar

mml

mml

mml

mml

mml

mml

mml

02jar.tex; 25/05/2002; 14:42; p.58

Continuous Latti es in

Mizar

59

31. L. S. van Benthem Jutting. Che king Landau's \Grundlagen" in the Automathsystem. THE Eindhoven, PhD thesis, 1977.
32. John L. Kelley. General Topology. van Nostrand, New York, 1955.
33. Artur Kornilowi z. Cartesian produ ts of relations and relational stru tures.
Formalized Mathemati s, 6(1):145{152, 1997.
: YELLOW 3.
34. Artur Kornilowi z. On the topologi al properties of meet- ontinuous latti es.
Formalized Mathemati s, 6(2):269{277, 1997.
: WAYBEL 9.
35. E. G. H. Landau. Grundlagen der Analysis. Akademis he Verlag, Leipzig,
1930.
36. Library Committee of the Asso iation of Mizar Users. Preliminaries toStru tures. Journal of Formalized Mathemati s, Addenda.
: STRUCT 0.
37. Library Committee of the Asso iation of Mizar Users. Preliminaries toArithmeti . Journal of Formalized Mathemati s, Addenda.
: ARYTM.
38. Beata Madras. Produ t of family of universal algebras. Formalized Mathemati s, 4(1):103{108, 1993.
: PRALG 1.
39. Robert Milewski. Algebrai latti es. Formalized Mathemati s, 6(2):249{254,1997.
: WAYBEL 8.
40. R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer. Sele ted papers on
Automath. North-Holland, Amsterdam, 1994.
41. Beata Padlewska and Agata Darmo hwal. Topologi al Spa es and Continuous
Fun tions. Formalized Mathemati s, 1(1):223{230, 1990.
: PRE TOPC.
42. H. Rasiowa and R. Sikorski The Mathemati s of Metamathemati s PWN,
Warszawa, 1968.
43. P. Rudni ki. Obvious inferen es. Journal of Automated Reasoning, 3:383{393,1987.
44. Piotr Rudni ki. Kernel proje tions and quotient latti es. Formalized Mathemati s, 7(2):169{175, 1998.
: WAYBEL20.
45. P. Rudni ki, Ch. S hwarzweller and A. Trybule . Commutative Algebra in the
Mizar System. Journal of Symboli Computation, 32:143{169, 2001.
46. Piotr Rudni ki and Andrzej Trybule . On equivalents of well-foundedness.
Journal of Automated Reasoning, 23(3-4):197{234, 1999.
47. Alexander Yu. Shibakov and Andrzej Trybule . The Cantor set. Formalized
Mathemati s, 5(2):233{236, 1996.
: CANTOR 1.
48. Andrzej Trybule . Tarski Grothendie k set theory. Formalized Mathemati s,
1(1):9{11, 1990.
: TARSKI.
49. Andrzej Trybule . Built-in on epts. Formalized Mathemati s, 1(1):13{15,1990.
: AXIOMS.
50. Andrzej Trybule . Categories without uniqueness of od and dom. Formalized
Mathemati s, 5(2):259{267, 1996.
: ALTCAT 1.
51. Andrzej Trybule . Fun tors for alternative ategories. Formalized Mathemati s,
5(4):595{608, 1996.
: FUNCTOR0.
52. Andrzej Trybule . Moore-Smith onvergen e. Formalized Mathemati s,
6(2):213{225, 1997.
53. Andrzej Trybule . S ott topology. Formalized Mathemati s, 6(2):311{319,1997.
: WAYBEL11.
54. Andrzej Trybule . Non Negative Real Numbers, Part I. Journal of Formalized
Mathemati s, Addenda.
: ARYTM 2.
55. Andrzej Trybule . Non Negative Real Numbers, Part II. Journal of Formalized
Mathemati s, Addenda.
: ARYTM 1.
56. Woj ie h A. Trybule . Partially ordered sets. Formalized Mathemati s,
1(2):313{319, 1990.
: ORDERS 1.

mml
mml

mml
mml

mml

mml

mml

mml

mml

mml

mml

mml

mml

mml

mml
mml
mml

02jar.tex; 25/05/2002; 14:42; p.59

60

G. Ban erek and P. Rudni ki

 e zkowska. Boolean properties of sets.
57. Zinaida Trybule and Halina SwiFormalized Mathemati s, 1(1):17{23, 1990.
: BOOLE.
58. Freek Wiedijk. Mizar: An Impression. http://www. s.kun.nl/~freek/notes.
59. Freek Wiedijk. Estimating the Cost of a Standard Library for a Mathemati al
Proof Che ker. http://www. s.kun.nl/~freek/notes.
60. Freek Wiedijk. The de Bruijn fa tor. http://www. s.kun.nl/~freek/notes.
61. Edmund Woronowi z. Relations de ned on sets. Formalized Mathemati s,
1(1):181{186, 1990.
: RELSET 1.
62. Edmund Woronowi z and Anna Zalewska. Properties of Binary Relations.
Formalized Mathemati s, 1(1):85{89, 1990.
: RELAT 2.
_
63. Stanislaw Zukowski.
Introdu tion to latti e theory. Formalized Mathemati s,
1(1):215{222, 1990.
: LATTICES.

mml

mml

mml

mml

Appendix
A. The

The items of theexamples.

l-book|WAYBEL orresponden el-book not mentioned below are either exer ises or

Chapter O. A Primer of Complete Latti es

pages

items

arti leauthor(s)

1{3
4
4
4{5
8{14
18{23
23{24
24{25
30{31
32

1.1{1.5
1.6
1.7
1.8{1.10
2.1{2.8
3.1{3.12
3.13{3.14
3.15{3.20
4.1{4.3
4.4

WAYBEL 0
LATTICE3
RELSET 1
WAYBEL 0
LATTICE3
WAYBEL 1
WAYBEL10
WAYBEL 1
WAYBEL 2
WAYBEL 9

G. Ban erek.
G. Ban erek LATTICE3 [4℄E. Woronowi z RELSET 1 [61℄G. Ban erek.
G. Ban erek LATTICE3 [4℄Cz. Bylinski.
G. Ban erek
Cz. Bylinski.
A. Kornilowi z
A. Kornilowi z

Chapter I. Latti e Theory of Continuous Latti es

pages

items

arti leauthor(s)

38{42
43{47
51
52

1.1{1.8
1.9{1.19
1.23
1.27

WAYBEL 3
WAYBEL 4
WAYBEL 4
WAYBEL 4

G. Ban erek
A. Grabowski
A. Grabowski
A. Grabowski

02jar.tex; 25/05/2002; 14:42; p.60

Continuous Latti es in

57{60
60
60
61
61
60{62
63
63
69{72
73{77
82{84
85{87
87
87
88{89
89{90
90{91
91{92
92{93

2.1{2.6
2.7
2.8
2.9
2.10
2.11{2.13
2.14
2.15
3.1{3.15
3.16{3.27
3.43
4.1{4.9
4.10
4.11
4.12{4.15
4.16
4.17
4.18
4.19{4.24

Mizar
M. Zynel

61_
WAYBEL 5
WAYBEL 5, WAYBEL20
WAYBEL20
P. Rudni ki
WAYBEL10
G. Ban erek
WAYBEL15
R. Milewski
WAYBEL20
P. Rudni ki
WAYBEL15
R. Milewski
WAYBEL20
P. Rudni ki
B. Madras
WAYBEL 6
G. Ban erek
WAYBEL 7
WAYBEL12
A. Kornilowi z
WAYBEL 8
R. Milewski
WAYBEL13
R. Milewski
WAYBEL 8
R. Milewski
WAYBEL13
R. Milewski
WAYBEL15
R. Milewski
WAYBEL22
P. Rudni ki
WAYBEL15
R. Milewski
WAYBEL16
R. Milewski

Chapter II. The S ott Topology

pages

items

arti leauthor(s)98{105105{108108{109112{113115{116116{117
115{117118
121{123123{126
128{130130{133
133{137

1.1{1.10
1.11{1.15
1.16{1.17
2.1{2.2
2.5{2.8
2.9
2.5{2.10
2.11
3.1{3.4
3.5{3.12
4.1{4.9
4.10{4.11
4.12{4.19

WAYBEL11
WAYBEL14
WAYBEL32
WAYBEL17
WAYBEL27
WAYBEL24
WAYBEL27
WAYBEL11
WAYBEL18
WAYBEL25
WAYBEL26
WAYBEL29

A. Trybule
Cz. Bylinski, P. Rudni ki
E. Gradzka
A. Grabowski
G. Ban erek, A. Naumowi z
A. Grabowski
G. Ban erek, A. Naumowi z(not nished)
J. Gryko
A. Kornilowi z, J. Gryko
G. Ban erek
G. Ban erek, A. Naumowi z
not done

02jar.tex; 25/05/2002; 14:42; p.61

62

G. Ban erek and P. Rudni ki

Chapter III. The Lawson Topology

pages

items

arti leauthor(s)142{145145{146
146{146
146{147153{156156
158{159
159
160{163
168{169
170{171
171{175

1.1{1.6
1.7{1.8
1.9{1.10
1.11
2.1{2.13
2.16
3.1{3.3
3.4{3.6
3.7{3.13
4.1{4.4
4.5{4.7
4.8{4.17

WAYBEL19
WAYBEL21
WAYBEL19
WAYBEL21
WAYBEL30
WAYBEL30
WAYBEL28
WAYBEL33

G. Ban erek
G. Ban erek
G. Ban erek
G. Ban erek
A. Kornilowi z
A. Kornilowi z
B. Skorulski
G. Ban erek, N. Endou
not doneR. Milewski
R. Milewski
not done

WAYBEL23
WAYBEL31

The formalization of Chapter IV of the l-book has begun reently and so far pp. 179{183, items 1.1{1.12 have been overed by
G. Ban erek in WAYBEL34.
Address for O prints: Piotr Rudni ki
Department of Computing S ien e
University of Alberta
Edmonton, Alberta, Canada T6G 2E8.

02jar.tex; 25/05/2002; 14:42; p.62