The Lattice of Topological Domains :An Example of Mizar Development
Zbigniew Karno
Institute of Mathematics
Warsaw University in Bialystok
15-267 Bialystok, Akademicka 2, Poland
Abstract

We present the complete development of the theory of topological domains (regularsets) in the Mizar formalism. It enveloped the lattice-theoretic foundations of the theory of domains that was given in [23] and in [12]. The aim is to present the main resultin [11] concerning certain characterizations of an extremally disconnected topologicalspace by means of properties of the lattice of domains and the main result in [12] concerning completeness of the lattice of domains of a topological space. Beforehand incomparison with a mathematical vernacular we present the mizared de nitions of all
useful notions and the all theorems which are necessary to the explanations.
The development presented here uses extracts of articles in the Main Mizar Library(MML), which have been fully checked by the PC Mizar System (Version 3.37). Therefore, we formulate only all de nitions and all theorems without the proof justi cations.
The full articles with proofs are available in the MML distributed together with the
PC Mizar System.

Contents

1 Introduction
2 Topological spaces in Mizar

23

3 Special topological spaces

8

4 Lattices in Mizar

13

5 Lattices of domains of a topological space

22

6 The lattice of domains of an extremally disconnected space29

2.1 Mizared de nition of topological spaces : : : : : : : : : : : : : : : : : : : : : 3
2.2 Subsets and subspaces in topological spaces : : : : : : : : : : : : : : : : : : : 4
2.3 Domains in topological spaces : : : : : : : : : : : : : : : : : : : : : : : : : : : 6
3.1 Discrete spaces : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 8
3.2 Extremally disconnected spaces : : : : : : : : : : : : : : : : : : : : : : : : : : 10

4.1 Mizared de nition of lattices : : : : : : : : : : : : : : : : : : : : : : : : : : : 13
4.2 Special lattices : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 16
4.3 Complete lattices : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 21
5.1 The lattice of domains : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 22
5.2 The lattices of closed domains and of open domains : : : : : : : : : : : : : : 24
5.3 Sublattices of the lattice of domains : : : : : : : : : : : : : : : : : : : : : : : 27
5.4 Completeness of the lattices of domains : : : : : : : : : : : : : : : : : : : : : 28

1

1 Introduction
The purpose of this paper is to give the complete development of the theory of topologicaldomains in the Mizar formalism. It should be noted that our approach has lattice{theoretic
foundations. Therefore, we rst present necessary parts of the theory of topological spaces([6], [7]) and the theory of lattices ([24], [1]) which are available in the Main Mizar Library(MML). We next present the main result in [11] on certain characterizations of an extremallydisconnected topological space by means of properties of the lattice of domains and themain result in [12] on completeness of the lattice of domains of a topological space. Because
recently the library evolves quite fast, it should be mentioned, that it is the stage of the
MML that ts the 3.37 version of the PC Mizar System.
The theory of closed and of open domains has been introduced by Kuratowski [15] inconnection with the closure and the interior operations in topological spaces and by Stone[19] in connections with the theory of Boolean algebras. Subsequently, it has been extensively
investigated by several authors (see e.g. Birkho [2], Tarski [21], MacNeille [17]).
Let us recall the concepts of closed and of open domains. Let X be a topological spaceand let A be a subset of X . A is said to be a closed domain (or regularly closed set ) if
A = Int A, and A is said to be an open domain (or regularly open set ) if A = Int A (see e.g.
[15], [13]). In the family of all closed domains in X let us de ne two binary operations _and ^ in the following way : A _ B = A [ B and A ^ B = Int (A \ B ), where A and B are
arbitrary closed domains. Similarly, in the family of all open domains in X let us de ne twobinary operations _ and ^ in the following way : A _ B = Int A [ B and A ^ B = A \ B ,where A and B are arbitrary open domains. It is well known (see e.g. [2], [16]) that for agiven topological space all its closed domains with operations _ and ^ de ned above form
a complete Boolean lattice, and similarly all its open domains with analogous operations _and ^ form a complete Boolean lattice, too.
A simple generalization of the notions of closed and of open domains is the following
one : A is said to be a domain (or a regular set ) in X provided Int A  A  Int A (see [7]and compare [10] where a domain is called a condensed set ). Of course, any closed domain
is a domain and any open domain is a domain, too.
In [23] and [12] certain connections between these concepts of domains have been introduced and studied. In particular, in the family of all domains of a given topologicalspace X two binary operations _ and ^ have been de ned. They are de ned as follows :A _ B = Int A [ B [ (A [ B ) and A ^ B = Int (A \ B ) \ (A \ B ), where A and B are arbitrary
domains in X . In [23] it has been proved that all domains of a given topological space withthe operations _ and ^ de ned above form a complemented lattice. In the same paper it
has been shown that both the lattice of open domains and the lattice of closed domains
are sublattices of the lattice of all domains. In [12] it has been proved an extension of ananalogous theorem for the lattices of closed and of open domains; namely that the latticeof all domains of a given topological space is complete.
In [11] a condition whether the lattice of all domains of a given topological space isBoolean has been formulated. To present that one we rst recall a de nition of a classof topological spaces which is important here. A topological space X is called extremallydisconnected if for every open subset A of X the closure A is open in X [20] (comp. [14],[8]). In [11] the following characterization has been obtained. The lattice of all domains of
a topological space X is modular if and only if X is extremally disconnected. Moreover,for every extremally disconnected space the lattice of all its domains coincide with both thelattice of all its closed domains and the lattice of all its open domains. Using these facts thefollowing characterization of extremally disconnected spaces generalizing the previous one
has been obtained. Namely, the lattice of all domains of a topological space X is Boolean if
and only if X is extremally disconnected. The aim here is to present of these results using
the Mizar formalism.
The paper is written for people who are a little more familiar with the Mizar language;
hence, a casual reader may have to refer rst to some of the cited paper e.g. [22], [3].
2

2 Topological spaces in Mizar
In this section we present all necessary facts on topological spaces formulated in the Mizar
formalism. To the explanation we use extracts of the articles [6] and [7], which are available
in the MML.

2.1 Mizared de nition of topological spaces

We mean by a topological space (see [13] and comp. [8]) a pair (X; T ) consisting of a set X
and a family T of subsets of X satisfying the following conditions :(1) X 2 T ;(2) if U1 2 T and U2 2 T , then U1S\ U2 2 T ;(3) if U is a subfamily of T , then U 2 T .
The set X is called a space and the family T is called the topology of X . The elements of
X are called points of the space, and the subsets of X are called subsets of the space. A
subset of the space X belonging to T is called open and its complement is called closed.
In Mizar the de nition of a topological space is somewhat di erent than this one given
above and has been done in three succeeding steps. It has been de ned rst a two elds
structure mode called TopStruct, which has as a pre x the structure mode 1-sorted. It
looks as follows (see [6]).
struct(1-sorted) TopStruct (# carrier -> non-empty set,
topology -> Subset-Family of the carrier #);In the structure de nition there occur two symbols of selectors : carrier and topology.
The symbol carrier corresponds to the rst eld of this structure and the symbol topology
corresponds to the second one. Thus the carrier and the topology are eld terms andthe rst one has the type non-empty set and the second one has the type Subset-Familyof the carrier. Observe that the eld term the carrier there occurs in the pattern ofthat structure mode. Now if X has a type which widens to the type TopStruct, then the
carrier of X and the topology of X are selector terms and the rst one has the typenon-empty set and the second one has the type Subset-Family of the carrier of X.
In the next step, we can de ne for every structure of a type which widens to the type
TopStruct the attribute TopSpace-like, using the Clustered Attribute De nition. Everysuch attributed structure must satis ed all of the conditions (1), (2) and (3) given above.
It has been done in the following way (comp. [6]).
definition mode TopSpace-like -> TopStruct means :: PRE TOPC:def 1
the carrier of it
the topology of it &(for F being Subset-Family of the carrier of it stF
the topology of it holds
union F the topology of it) &(for A,B being Subset of the carrier of it stA
the topology of it & B
the topology of it holds
AB
the topology of it);
end;

2



2

2
\ 2

2

In a correctness condition to this de nition the existence of a structure of the typehas been justi ed. In e ect this de nition produces an existential cluster, which ensures that the class of all structures of the type TopSpace-like
TopStruct is nonempty. Now, every structure of a type which widens to the type TopSpace-like TopStruct is a structure satisfying all of the conditions given in the de nition of a
topological space. So, in the last step we can de ne the notion of a topological space as the
TopSpace-like TopStruct3

type TopSpace coinciding with the type TopSpace-like TopStruct using the Expandable

Mode De nition. It looks as follows (comp. [6]).

definition mode TopSpace is TopSpace-like TopStruct;end;

The existential cluster has been constructed next, which ensures that the class of all
structures of the type TopSpace with the attribute strict, hence the class of all structuresof the type TopSpace, is nonempty.
definition
cluster strict TopSpace;end;

Note that the meaning of the attribute strict in Mizar is very dicult to explain (see[22]). It requires a separate presentation, and in this paper it will be omitted.
To complete this subsection let us draw the following tree of the Mizar types. Here andsubsequently the arrow indicates the direction of widening of types provided automaticallyby the Mizar System.

 
6TopStructTopSpace-like TopStruct

= 


TopSpace

2.2 Subsets and subspaces in topological spaces

In [6], using the Expandable Mode De nition, the types Point of X and Subset of X havebeen introduced. But earlier the identi er X of the type TopSpace has been reserved. The
reservation xes X for a structure of the type TopSpace either in a whole Mizar article (i.e.
from the reservation to the end of an article) or in its part till to a next reservation of thesame identi er.
reserve X for TopSpace;definition let X;
mode Point of X is Element of the carrier of X;
end;

4

definition let X;
mode Subset of X is set of Point of X;
end;

Next, using the Functor De nition, two functors ;(X) and (X) have been de ned. They
have the type Subset of X. From the theorems presented below it follows that ;(X) equals; and (X) equals the carrier of X. But neither ; nor the carrier of X do not havethe type Subset of X.
definition let X;
func (X) -> Subset of X means :: PRE TOPC:def 2
it = the carrier of X;
func (X) -> Subset of X means :: PRE TOPC:def 3
it =the carrier of X;
end;

;

;

theorem :: PRE TOPC:11(T) = ;;;

theorem :: PRE TOPC:12(X) = the carrier of X;

Using the Predicate De nition, two predicates A is open and A is closed have beende ned. But rst the identi er A of the type Subset of X has been reserved globally.
reserve A for Subset of X;
definition let X,A;
pred A is open means :: PRE TOPC:def 4
A
the topology of X;
end;

2

definition let X,A;
pred A is closed means :: PRE TOPC:def 5(X) n A is open;
end;

Next, using the Functor De nition, two functors Cl A and Int A of the type Subset ofhave been introduced, the rst one in [6] and the second one in [7]. These functors yield
the closure and the interior in an arbitrary topological space (comp. [15], [13] and [8]).
X

definition let X be TopSpace, A be Subset of X;
func Cl A -> Subset of X means :: PRE TOPC:def 11
for p being Point of X holdsp
it iff for G being Subset of X st G is open holds
p G implies A
G <> (X);
end;

2

2

definition let X be TopSpace, A be Subset of X;

5

\

;

func Int A -> Subset of X means :: TOPS_1:def 1
it = (Cl(A`))`;
end;

It should be noted that in the above de nition A` means the complement of A in X.
The operations Cl and Int have a lot of remarkable properties; they may be found in
the MML in [6], [7], [23] and [12].
In [6], using the Mode De nition, the type SubSpace of X has been de ned. Afterwards
the existential cluster for this type has been done.
definition let X;
mode SubSpace of X -> TopSpace means :: PRE TOPC:def 8
(it)
(X) &
for P being Subset of it holds P the topology of it iff
ex Q being Subset of X st Q
the topology of X & P = Q
end;



2

2

\ (it);

definition let X;
cluster strict SubSpace of X;
end;

2.3 Domains in topological spaces

In [7], using the Predicate De nition, three predicates A is domain, A is closed domain
and A is open domain have been introduced. Of course, the mizared de nitions of thesepredicates are just the same as those given in the introduction.
definition let X,A;
pred A is domain means :: TOPS 1:def 6Int(Cl A)
A & A
Cl(Int A);
pred A is closed domain means :: TOPS 1:def 7
A = Cl(Int A);
pred A is open domain means :: TOPS 1:def 8
A = Int(Cl A);
end;





Based on [7] and [23], we present below selected properties of domains, closed domains
and open domains (comp. [15], [13], [16]).
theorem :: TOPS_1:106
A is_closed & A is_domain iff A is_closed_domain;

theorem :: TOPS_1:107

6

A is_open & A is_domain iff A is_open_domain;

theorem :: TOPS 1:108
A is closed domain & B is closed domain implies A
theorem :: TOPS 1:109
A is open domain & B is open domain implies A[ B is closed domain;\ B is open domain;

theorem :: TOPS_1:111
A is_domain implies Int A is_domain & Cl A is_domain;

theorem :: TDLAT_1:16
for A being Subset of X st A is_domain holds A` is_domain;

theorem :: TDLAT 1:17
for A,B being Subset of X st A is domain & B is domain holds
Int(Cl(A B)) (A B) is domain & Cl(Int(A B)) (A B) is domain;

[

[

\

[

\

\

theorem :: TDLAT_1:22
for A being Subset of X holds Cl(Int A) is_closed_domain;

theorem :: TDLAT_1:23
for A being Subset of X holds Int(Cl A) is_open_domain;

theorem :: TDLAT_1:24
for A being Subset of X st A is_domain holds Cl A is_closed_domain;

theorem :: TDLAT_1:25
for A being Subset of X st A is_domain holds Int A is_open_domain;

theorem :: TDLAT_1:26
for A being Subset of X st A is_domain holds Cl A` is_closed_domain;7

theorem :: TDLAT_1:27
for A being Subset of X st A is_domain holds Int A` is_open_domain;

Note that in [12] the closure and the interior operations for families of subsets of topological spaces have been introduced and their important properties have been presented(comp. [13], [15]). Using these notions, certain properties of domains, closed domains andopen domains have been studied (comp. [15], [13], [16], [8]).

3 Special topological spaces
In this section, based on [11], we present some of the standard facts on discrete, antidiscrete, almost discrete, extremally disconnected and hereditarily extremally disconnected
topological spaces formulated in the Mizar formalism (comp. [14], [8]).

3.1 Discrete spaces

We start with presentation of discrete topological structures in Mizar. In [11], using the
Attribute De nition, for every structure of a type which widens to the type TopStruct the
attributes discrete and anti-discrete have been introduced. It has been done as follows.
definition
attr discrete -> TopStruct means :: TDLAT 3:def 1
the topology of it = bool the carrier of it;
attr anti-discrete -> TopStruct means :: TDLAT 3:def 2
the topology of it =, the carrier of it ;
end;

f;

g

Note that bool A means in Mizar the power set of A.
The existential cluster has been done next, which guarantees that the class of all structures of the type TopStruct with the attributes discrete anti-discrete strict, hence
the class of all structures of the type discrete anti-discrete TopStruct, is nonempty.
It looks as follows.
definition
cluster discrete anti-discrete strict TopStruct;end;

Afterwards two conditional clusters have been de ned and proved. The rst one ensuresthat every type which widens to the type discrete TopStruct widens also to the type
TopSpace-like TopStruct and hence to the type TopSpace. Similarly, the second one
ensures that every type which widens to the type anti-discrete TopStruct widens also
to the type TopSpace-like TopStruct and hence to the type TopSpace.
definition
cluster discrete -> TopSpace-like TopStruct;8

cluster anti-discrete -> TopSpace-like TopStruct;
end;

Next, for every structure of a type which widens to the type TopStruct the attributehas been introduced.

almost discrete

definition
attr almost discrete -> TopStruct means :: TDLAT 3:def 3
for A being Subset of the carrier of it stA
the topology of it holds(the carrier of it) n A the topology of it;
end;

2

2

Then two conditional clusters have been de ned and proved. These ones ensure that every type which widens either to the type discrete TopStruct or to the type anti-discrete
TopStruct widens also to the type almost discrete TopStruct.
definition
cluster discrete -> almost_discrete TopStruct;cluster anti-discrete -> almost_discrete TopStruct;end;

Afterwards the existential cluster has been constructed, which guarantees that the classof all structures of the type almost discrete strict TopStruct, hence the class of all
structures of the types almost discrete TopStruct, is nonempty.
definition
cluster almost_discrete strict TopStruct;
end;

 



@I
@



 6  HYHH*
6
 HH






The net of the types de ned above looks like this.
TopStruct

TopSpacealmost discrete TopStructdiscrete TopStructanti-discrete TopStruct

9






We can now present discrete topological spaces in Mizar. In [11], the following two
existential clusters have been constructed. The rst one guarantees that the class of all
structures of the type discrete anti-discrete TopSpace is nonempty and the second
one guarantees that the class of all structures of the type almost discrete TopSpace isnonempty.
definition
cluster discrete anti-discrete strict TopSpace;cluster almost_discrete strict TopSpace;
end;

Then two conditional clusters have been de ned and proved. These ones ensure that every type which widens either to the type discrete TopSpace or to the type anti-discrete
TopSpace widens also to the type almost discrete TopSpace.
definition
cluster discrete -> almost_discrete TopSpace;cluster anti-discrete -> almost_discrete TopSpace;
end;

 
6 

Now the tree of these types looks like this.
TopSpace






@I

almost discrete TopSpace

discrete TopSpace

  @
 

anti-discrete TopSpace

3.2 Extremally disconnected spaces

The mizared de nition of extremally disconnected topological spaces has been done in [11].
Using the Attribute De nition, for every structure of a type which widens to the type
TopSpace the attribute extremally disconnected has been introduced as in the de nition
presented below. The de niens of this de nition is the same as in the well known de nitionof extremally disconnected spaces [19] (comp. [14] or [8]).
definition
attr extremally disconnected -> TopSpace means :: TDLAT 3:def 4

10

for A being Subset of it st A is open holds Cl A is open;
end;

Then the following existential cluster has been constructed. It guarantees, in particular, that the class of all structures of the type extremally disconnected TopSpace isnonempty.
definition
cluster extremally_disconnected strict TopSpace;end;

Any extremally disconnected topological space can be characterized by certain propertiesof the family of all its domains. Some of these ones are listed in the theorems given below(see [11]).
reserve X for TopSpace;

theorem :: TDLAT_3:34
X is extremally_disconnected iff
for A being Subset of X st A is_domain holds A is_closed & A is_open;

theorem :: TDLAT_3:35
X is extremally_disconnected iff
for A being Subset of X st A is_domain holds
A is_closed_domain & A is_open_domain;

theorem :: TDLAT_3:36
X is extremally_disconnected iff
for A being Subset of X st A is_domain holds Int Cl A = Cl Int A;

theorem :: TDLAT_3:38
X is extremally_disconnected iff
for A being Subset of X holds

11

(A is_open_domain implies A is_closed_domain) &(A is_closed_domain implies A is_open_domain);

It is well known that there exists an extremally disconnected topological space with asubspace which is not extremally disconnected (see e.g. [8]). So, the de nition of the type
TopSpace with the attribute hereditarily extremally disconnected is sensible. It has
been done in [11] as follows.
definition
attr hereditarily_extremally_disconnected ->TopSpace means :: TDLAT_3:def 5
for X0 being SubSpace of it holds X0 is extremally_disconnected;
end;

Afterwards the existential cluster for the type hereditarily extremally disconnected
has been constructed.

TopSpace

definition
cluster hereditarily_extremally_disconnected strict TopSpace;
end;

Then two conditional clusters have been de ned. The rst one guarantees that every
type which widens to the type hereditarily extremally disconnected TopSpace widens
also to the type extremally disconnected TopSpace. The second one guarantees thatevery type which widens to the type almost discrete TopSpace widens also to the type
hereditarily extremally disconnected TopSpace.
definition
clusterhereditarily_extremally_disconnected -> extremally_disconnected TopSpace;clusteralmost_discrete -> hereditarily_extremally_disconnected TopSpace;end;

So, the previous tree of types extends to the following one.
12

 
6 
TopSpace

extremally disconnected TopSpace

6

hereditarily extremally disconnected TopSpace

6

almost discrete TopSpace







Remarks. The clustering constructions are very useful in Mizar. For instance thefollowing Mizar sentencefor X being almost_discrete TopSpace holds
X is extremally_disconnected;

is obvious for the Mizar System. Moreover, the following sentencefor X being discrete TopStruct holds
X is hereditarily_extremally_disconnected TopSpace;is also obvious (note that in it TopSpace can be dropped).

4 Lattices in Mizar
In this section we present all necessary facts from the theory of lattices formulated in the
Mizar formalism. To the explanation we use extracts of the articles [24] and [1], which areavailable in the MML.

4.1 Mizared de nition of lattices

We mean by a lattice (see [2], [9] and comp. [4]) a nonempty set L together with two binary
operations _ and ^ de ned on L satisfying the following conditions :(1) a _ b = b _ a and a ^ b = b ^ a;(2) a _ (b _ c) = (a _ b) _ c and a ^ (b ^ c) = (a ^ b) ^ c;(3) a = a _ (a ^ b) and a = a ^ (a _ b);(4) a _ a = a and a ^ a = a.
The operations _ and ^ are called the join and the meet, respectively. It should be notedthat there is the other way of de ning lattices, based on the notion of order (see [2]).
13In Mizar the de nition of lattices is quite similar to given above. It has been done inseveral steps. First, a three elds structure mode called LattStr with the pre x 1-sorted
has been constructed. Then, the attribute Lattice-like for the type LattStr, which forms
the type Lattice, has been de ned.
The structure de nition of LattStr looks as follows (comp. [24]).
struct(1-sorted) LattStr  carrier -> non-empty set,
L join,L meet -> BinOp of the carrier ;

In the de nition of this structure mode there occur the following three symbols of selectors of elds : carrier, L join and L meet. If G has a type which widens to the type
LattStr, then the selector term the carrier of G has the type non-empty set and theselector terms the L join of G and the L meet of G have the type of the BinOp of thecarrier of G. Here every function of the type BinOp of A has in Mizar the meaning of abinary operation on the set A (i.e. has the type Function of [:A,A:],A).
Using the Functor De nition, for given structure G of the type LattStr two functors
p t q and p u q of the type Element of the carrier of G have been de ned. These
ones correspond to the binary operations _ and ^, respectively, given above. But earlier
the identi ers G of the type LattStr and p, q of the type Element of the carrier of G
have been reserved globally.
reserve G for LattStr;
reserve p,q for Element of the carrier of G;
definition let G,p,q;
func p q -> Element of the carrier of G means :: LATTICES:def 1
it = (the L join of G).(p,q);
func p q -> Element of the carrier of G means :: LATTICES:def 2
it = (the L meet of G).(p,q);
end;

t

u

Next, using the Predicate De nition, for given structure G of the type LattStr thepredicate p  q has been introduced. It corresponds to a relation, which will has beende ned a partial order in every structure of the type Lattice.
definition let G,p,q;
pred p  q means :: LATTICES:def 3p
q = q;end;t

For given structure G of the type LattStr the type Subset of G can be de ned. It has
been done in [1], using the Expandable Mode De nition.
definition let G be LattStr;
mode Subset of G is Subset of the carrier of G;
end;

We are ready now to give the de nition of lattices in Mizar. We can de ne for every
structure of a type which widens to the type LattStr the attribute Lattice-like with the14

de niens given by (1) - (3), using the Clustered Attribute De nition. It has been done asfollows (comp. [24]).
definitionmode Lattice-like -> LattStr means :: LATTICES:def 4(for a,b being Element of the carrier of it holds a
b = b
a) &
(for a,b,c being Element of the carrier of it
holds a (b c) = (a b) c) &(for a,b being Element of the carrier of it holds (a b) b = b) &(for a,b being Element of the carrier of it holds a b = ba) &(for a,b,c being Element of the carrier of it
holds a (b c) = (a b) c) &(for a,b being Element of the carrier of it holds a(ab) = a);
end;

t

t

u

t

u

u
u

u

t

t

u

t

t

t

u

u

Now every structure of a type which widens to the type Lattice-like LattStr isa structure satisfying all of the conditions given in the de nition of a lattice. So, we canintroduce the notion of a lattice as the type Lattice coinciding with the type Lattice-like
LattStr, using the Expandable Mode De nition. It has been done as follows (comp. [6]).
definitionmode Lattice is Lattice-like LattStr;
end;

In a correctness condition to previous de nition the existence of a structure of the typehas been proved. In e ect that de nition produces an existential
cluster, which guarantees that the class of all structures of the type Lattice-like LattStr
is nonempty. On the other hand the following existential cluster has been constructed. It
guarantees that the class of all structures of the type strict Lattice, hence the class ofall structures of the type Lattice, is nonempty.
Lattice-like LattStr

definition
cluster strict Lattice;
end;



6 

The tree of the Mizar types de ned above looks like this.
LattStr

Lattice-like LattStr




=
 
LatticeIn [5], using the Mode De nition, for every structure L of a type which widens to thetype Lattice the type SubLattice of L has been introduced. Afterwards the existential
cluster for this type has been done.
15

definition let L be Lattice;mode SubLattice of L -> Lattice means :: NAT LAT:def 16
the carrier of it
the carrier of L &the L join of it =(the L join of L)|[:the carrier of it,the carrier of it:] &the L meet of it =(the L meet of L)|[:the carrier of it,the carrier of it:];end;definition let L be Lattice;cluster strict SubLattice of L;
end;

Note that in the previous de nition | is the restriction operation and [:A,B:] denotes the
Cartesian product of the sets A and B

4.2 Special lattices

In this subsection, based on [24], we present mizared de nitions of the distributive, modular,
complemented and Boolean lattices (comp. [2], [9]). Let us recall that a distributive lattice
is a lattice which satis es one of the equivalent conditions :(5) a ^ (b _ c) = (a ^ b) _ (a ^ c),(6) a _ (b ^ c) = (a _ b) ^ (a _ c).
In mizared de nition we use the rst one. Namely, we introduce for every structureof a type which widens to the type Lattice the attribute distributive, using Clustered
Attribute De nition. It has been done in the following way.
definitionmode distributive -> Lattice means :: LATTICES:def 5
for a,b,c being Element of the carrier of it
holds a (b c) = (a b) (a
c);
end;

u

t

u

t

u

We de ne next the type D Lattice as the type distributive Lattice, using the Expandable Mode De nition. Then we can construct the existential cluster for this type. It

has been done as follows.
definitionmode D_Lattice is distributive Lattice;end;definition
cluster strict D_Lattice;
end;

16

Let us recall that a modular lattice is a lattice which satis es the following conditions :(7) if a  b, then a _ (b ^ c) = a ^ (b _ c).
Mizared de nition of modularity is the same. Similarly as in the de nition of distributivity, we can introduce for every structure of a type which widens to the type Lattice theattribute modular with the de niens given by (7), using the Clustered Attribute De nition.
One can de ne next the type M Lattice as the type modular Lattice, using the Expandable Mode De nition. Then we can construct an existential cluster for this type. It has been
done as follows.
definitionmode modular -> Lattice means :: LATTICES:def 6
for a,b,c being Element of the carrier of it st a  cholds a (b c) = (a
end;

t

u

t b) u c;definitionmode M_Lattice is modular Lattice;end;definition
cluster strict M_Lattice;end;

Before the mizared de nition of complemented lattices we give rst the de nitions ofcertain special lattice elements. Using the Conditional Functor De nition, we can de ne for
given lattice L (of the type Lattice of course) two functors ? L and > L of the type Elementof the carrier of L. The rst one corresponds to the least element 0 and the second one
corresponds to the greatest element 1 in a bound lattice (comp. [9]). It has been done in[24] as follows.
reserve L for Lattice, a,b,c for Element of the carrier of L;
definition let L;
assume ex c st for a holds c a = c;func ? L -> Element of the carrier of L means :: LATTICES:def 10
it
a = it;end;uu

definition let L;
assume ex c st for a holds c a = c;func > L -> Element of the carrier of L means :: LATTICES:def 11
it
a = it;end;tt

In [24], the type 01 Lattice which extends to the type Lattice has been introduced.
It corresponds to the concept of bound lattices with the least element 0 and the greatest
17

element 1 (comp. [9]). Let us recall that in a bound lattice L two its elements a and b are
said to be complementary, whenever(8) a _ b = 1 and a ^ b = 0.
Any element complementary to a is called a complement of a in L (see e.g. [9]). This
concept has been de ned in Mizar similarly. It uses the Conditional Predicate De nition
and it is de ned as the predicate a is a complement of b with the de niens given by (8),where a,b have the type Element of the carrier of L and L has the type Lattice withthe permissivness condition : L is 01 Lattice. So, this predicate is de ned in fact to thetype 01 Lattice. Precisely, it looks as follows.
definition let L,a,b;
assume L is 01 Lattice;
pred a is a complement of b means :: LATTICES:def 12ab = > L & a b = ? L;
end;

t

u

We are ready now to de ne the concept of complemented lattices. Let us recall that(comp. [9]) a complemented lattice is a bound lattice which satis es the following conditions :(9) for every a there exists b such that a is complement of b.
This de nition in Mizar has been done in the same way (comp. [24]). First, using
the Clustered Attribute De nition, For every structure of a type which widens to the type01 Lattice the attribute complemented, with the de niens given by (9), has been introduced. Next, the type C Lattice as the type complemented 01 Lattice has been de ned
and the existential cluster for this type has been constructed.
definitionmode complemented -> 01_Lattice means :: LATTICES:def 13
for b being Element of the carrier of it
ex a being Element of the carrier of it st a is_a_complement_of b;
end;

definitionmode C_Lattice is complemented 01_Lattice;end;definition
cluster strict C_Lattice;end;

Let us recall that a Boolean lattice is any distributive complemented lattice (see [9] andcomp. [2]). In Mizar this de nition is just the same. Namely, for every structure of a type18

which widens to the type C Lattice the attribute Boolean, with the de niens which saysthat this structure is distributive, has been introduced (comp. [24]).
definitionmode Boolean -> C_Lattice means :: LATTICES:def 14
it is distributive;
end;

Afterwards the type B Lattice as the type Boolean C Lattice has been de ned andthe existential cluster for this type has been constructed.
definitionmode B_Lattice is Boolean C_Lattice;end;definition
cluster strict B_Lattice;end;

The tree of the lattice types looks like this.

19



 
 6 6




=
 





=
 

 
 6 

 = 6 =  Lattice

M Lattice

modular Lattice

D Lattice

distributive Lattice

01 Latticecomplemented 01 Lattice

C Lattice

B Lattice

Boolean C Lattice

Unfortunately the widening of the type D Lattice to the type M Lattice and the wideningof the type B Lattice to the type D Lattice are not supported automatically. Because
in the MML the corresponding conditional clusters do not exist. But these widenings areaccessible because of the following two theorems.
reserve L for D_Lattice;theorem :: LATTICES:35
L is modular;

reserve L for B_Lattice;theorem :: LATTICES:59
L is D_Lattice;

The second widening is accessible also by the de nitional expansion of the de nitionof the attribute Boolean (it is supported automatically), or by the de nitional theorem,
which is automatically created from the de nition of the attribute Boolean (here a label isneeded).
20

4.3 Complete lattices

Let
that a lattice is said to be complete if for every its subset A both the supremum
W Ausof recall
A and the in mum V A of A exist (see [2], [9]). Mizared de nition ofWcomplete lattices
is somewhat di erent. It uses in fact of the existence of the supremum A. It has been
done in [1] as follows. First, using the Predicate De nition, for given structure L of thetype LattStr two predicates p is less than A and A is less than p with the synonyms
A is great than p and p is great than A, respectively, have been introduced.

definition let L be LattStr, p be Element of L, A be set;
pred p is less than A means :: LATTICE3:def 16
for q being Element of L st q A holds p  q;
synonym A is great than p;
pred A is less than p means :: LATTICE3:def 17
for q being Element of L st q A holds q  p;synonym p is great than A;
end;

2
2

Then using the Attribute De nition, for every structure of a type which widens to thetype LattStr the attribute complete has been introduced as in the following de nition.
definition
attr complete -> LattStr means :: LATTICE3:def 18
for A being set
ex p being Element of it st A is less than p &for r being Element of it st A is less than r holds p  r;
end;

Afterwards using the AttributeW De nition, for every Vstructure of a type which widens to
the type LattStr two attributes -distributive and -distributive have been de ned
andthe following Vexistential cluster for the type Lattice with the attributes complete
W-distributive-distributive strict has been constructed. In particular, it ensuresthat the class of all structures of the type complete Lattice is nonempty.
definition
cluster complete
end;

W-distributive V-distributive strict Lattice;

Next, for every structure L of a type which widens to Wthe type LattStr
V and satisfying
the condition : L is complete Lattice, two functors (A,L) and (A,L) have been
introduced. They have meaning of the supremum and of the in mum, respectively.

W

definition let L be LattStr such that L is complete Lattice; let A be set;func (A,L) -> Element of L means :: LATTICE3:def 21
A is less than it &for r being Element of L st A is less than r holds it  r;
end;

V
Wf

definition let L be LattStr, A be set;func (A,L) -> Element of L means :: LATTICE3:def 22
it = ( p where p is Element of L : p is less than A ,L);end;g

The existence conditions to the both de nitions have been proved. These guaranteethat for every structure L of a type which widens
W to theVtype LattStr and satisfying thecondition : L is complete Lattice, both (A,L) and (A,L) exist. In particular, it isalso true for the structures of the type complete Lattice.
21

5 Lattices of domains of a topological space

5.1 The lattice of domains

We are ready now to introduce in Mizar the concept of the lattice of domains of a topologicalspace. It has been done by Toshihiko Watanabe in [23]. First, for a given topological space
X, i.e. for X of the type TopSpace (more for X of the type widens to the type TopSpace),
the aggregate
LattStr  Domains of X,Domains Union X,Domains Meet X 

has been constructed. It is created by application of the aggregate functor
LattStr ,,to the following list of functor terms Domains of X, Domains Union X and Domains Meet
. These functors, de ned below, have the required types as in the de nition of the structure mode LattStr given in the subsection 4.1. Namely, Domains of X has the typenon-empty set, and both Domains Union X and Domains Meet X have the type BinOp of
the Domains of X. So, this aggregate is a structure of the type LattStr.
Domains of X consists of all domains of the topological space X. Therefore in particular,
it has the type Subset-Family of the carrier of X. Precise Mizar de nition looks asfollows.
X

definition let X be TopSpace;func Domains_of X ->non-empty Subset-Family of the carrier of X means :: TDLAT_1:def 1
it = {A where A is Subset of X : A is_domain};
end;

Both Domains Union X and Domains Meet X are binary operations on Domains of X.
The value of the rst one is Int A [ B [ (A [ B ), and the value of the second one is
Int (A \ B ) \ (A \ B ), where A and B are arbitrary domains in X . Observe that thefunctor Domains Union X has the abbreviation D-Union X and the functor Domains Meet
X has the abbreviation D-Meet X.
definition let X be TopSpace;func Domains Union X -> BinOp of Domains of X means :: TDLAT 1:def 2
for A,B being Element of Domains of X holdsit.(A,B) = Int(Cl(A B))(A B);
synonym D-Union X;
end;

[

[

[

definition let X be TopSpace;func Domains Meet X -> BinOp of Domains of X means :: TDLAT 1:def 3
for A,B being Element of Domains of X holdsit.(A,B) = Cl(Int(A B))(A B);
synonym D-Meet X;
end;

\

22

\

\

Afterwards the following important theorem has been proved. We also give the skeletonof the Mizar proof of it.
theorem :: TDLAT 1:30
for X being TopSpace holds
LattStr  Domains of X,D-Union X,D-Meet X  is C Lattice;
proof let X be TopSpace;set L = LattStr  Domains of X,D-Union X,D-Meet X  ;L is Lattice@proof end;
then reconsider L as Lattice;
L is 01 Lattice@proof end;
then reconsider L as 01 Lattice;
L is C Lattice@proof end;
hence thesis;
end;This theorem says that the aggregate
LattStr  Domains of X,Domains Union X,Domains Meet X 

is a structure of the type C Lattice. So, we can introduce the functor Domains Lattice X,
which is a structure of the type complemented Lattice and it is equal to that aggregate.
Precise Mizar de nition has been done in [23] as follows.
definition let X be TopSpace;func Domains Lattice X -> C Lattice means :: TDLAT 1:def 4
it = LattStr  Domains of X,Domains Union X,Domains Meet X  ;end;Roughly speaking, Domains Lattice X is the (complemented) lattice of all domains of
the topological space X . Basic properties of this lattice are listed below.
theorem :: TDLAT_2:86
the carrier of Domains_Lattice X = Domains_of X;

theorem :: TDLAT 2:87
for a, b being Element of Domains Lattice X
for A, B being Element of Domains of X st a = A & b = B holdsab = Int(Cl(A B)) (A B) & a b = Cl(Int(A B))
(A
B);

t

[

[

[

u

theorem :: TDLAT 2:88
? (Domains Lattice X) = X & > (Domains Lattice X) =

;

\

\

\

X;

theorem :: TDLAT 2:89
for a, b being Element of Domains Lattice X
for A, B being Element of Domains of X st a = A & b = B holdsa  b iff A c= B;

23

5.2 The lattices of closed domains and of open domains

The concepts of the lattices of closed domains and of open domains of a topological spacehave been introduced in Mizar similarly as the lattice of domains (see [23] and comp. [2],[16]). For given X of the type TopSpace (more for X of a type which widens to the type
TopSpace) the aggregate
LattStr Closed Domains of X,Closed Domains Union X,Closed Domains Meet X corresponding to the lattice of closed domains and the aggregate
LattStr  Open Domains of X,Open Domains Union X,Open Domains Meet X corresponding to the lattice of open domains, are constructed. From the de nitions ofClosed Domains of X, CLD-Union X, CLD-Meet X, Open Domains of X, OPD-Union X and
OPD-Meet X it follows that these aggregates are structures of the type LattStr (note that
we use here the corresponding abbreviations of these functors). The de nitions of the above
mentioned functors have been done in Mizar as follows.
definition let X be TopSpace;func Closed_Domains_of X ->non-empty Subset-Family of the carrier of X means :: TDLAT_1:def 5
it = {A where A is Subset of X : A is_closed_domain};end;definition let X be TopSpace;func Open_Domains_of X ->non-empty Subset-Family of the carrier of X means :: TDLAT_1:def 9
it = {A where A is Subset of X : A is_open_domain};end;definition let X be TopSpace;func Closed Domains Union X ->BinOp of Closed Domains of X means :: TDLAT 1:def 6
for A,B being Element of Closed Domains of X holdsit.(A,B) = A
B;
synonym CLD-Union X;
end;[

definition let X be TopSpace;func Open Domains Union X ->BinOp of Open Domains of X means :: TDLAT 1:def 10
for A,B being Element of Open Domains of X holdsit.(A,B) = Int(Cl(A B));synonym OPD-Union X;

[

24

end;
definition let X be TopSpace;func Closed Domains Meet X ->BinOp of Closed Domains of X means :: TDLAT 1:def 7
for A,B being Element of Closed Domains of X holdsit.(A,B) = Cl(Int(A B));synonym CLD-Meet X;
end;\definition let X be TopSpace;func Open Domains Meet X ->BinOp of Open Domains of X means :: TDLAT 1:def 11
for A,B being Element of Open Domains of X holdsit.(A,B) = A
B;
synonym OPD-Meet X;
end;\

In [23], the following two theorems have been proved. Similarly as in the previous case,we give also the skeleton of the Mizar proof of the rst one. The skeleton of the Mizar proofof the second one looks the same.
theorem :: TDLAT 1:34
for X being TopSpace holds
LattStr  Closed Domains of X,CLD-Union X,CLD-Meet X  is B Lattice;
proof let X be TopSpace;set L = LattStr  Closed Domains of X,CLD-Union X,CLD-Meet X  ;L is Lattice@proof end;
then reconsider L as Lattice;
L is 01 Lattice@proof end;
then reconsider L as 01 Lattice;
L is C Lattice@proof end;
then reconsider L as C Lattice;
L is B Lattice
proofthus L is D Lattice@proof end;
end;
hence thesis;
end;theorem :: TDLAT 1:38
for X being TopSpace holds
LattStr  Open Domains of X,OPD-Union X,OPD-Meet X  is B Lattice;

It follows that the aggregates given above are structures of the type B Lattice. Thus
we can introduce the functors Closed Domains Lattice X and Open Domains Lattice X
as in the following de nitions.
definition let X be TopSpace;func Closed Domains Lattice X -> B Lattice means :: TDLAT 1:def 8

25

it =
LattStr  Closed Domains of X,Closed Domains Union X,Closed Domains Meet X ;
end;definition let X be TopSpace;func Open Domains Lattice X -> B Lattice means :: TDLAT 1:def 12
it = LattStr  Open Domains of X,Open Domains Union X,Open Domains Meet X ;
end;

Roughly speaking, for a topological space X the functors Closed Domains Lattice X
and Open Domains Lattice X have meaning of the (Boolean) lattice of all closed domainsof X and of the (Boolean) lattice of all open domains of X , respectively. Basic propertiesof these lattices are listed below.
theorem :: TDLAT_2:94
the carrier of Closed_Domains_Lattice X = Closed_Domains_of X;

theorem :: TDLAT_2:103
the carrier of Open_Domains_Lattice X = Open_Domains_of X;

theorem :: TDLAT 2:95
for a, b being Element of Closed Domains Lattice X
for A, B being Element of Closed Domains of X st a = A & b = B holdsab = A B & a b = Cl(Int(A B));

t

[

u

\

theorem :: TDLAT 2:104
for a, b being Element of Open Domains Lattice X
for A, B being Element of Open Domains of X st a = A & b = B holdsab = Int(Cl(A B)) & a
b = A
B;

t

[

u

\

theorem :: TDLAT 2:96
? (Closed Domains Lattice X) = X & > (Closed Domains Lattice X) =;theorem :: TDLAT 2:105? (Open Domains Lattice X) = X & > (Open Domains Lattice X) =

;

X;

X;

theorem :: TDLAT 2:97
for a, b being Element of Closed Domains Lattice X
for A, B being Element of Closed Domains of X st a = A & b = B holdsa  b iff AB;theorem :: TDLAT 2:106
for a, b being Element of Open Domains Lattice X
for A, B being Element of Open Domains of X st a = A & b = B holdsa  b iff A
B;



26

5.3 Sublattices of the lattice of domains

The lattices of all closed domains and of all open domains of a given topological space aresublattices of the lattice of all domains. It has been proved in [23].
First, it has been proved in fact that the carrier of Closed Domains Lattice X 
the carrier of Domains Lattice X and the carrier of Open Domains Lattice X 
the carrier of Domains Lattice X.

theorem :: TDLAT 1:31
for X being TopSpace holds Closed Domains of X
theorem :: TDLAT 1:35
for X being TopSpace holds Open Domains of X

 Domains of X;

 Domains of X;

Next, the following connections between lattice operations in the lattices of domains :,and Open Domains Lattice X, have been
observed.
Domains Lattice X Closed Domains Lattice X

theorem :: TDLAT_1:32
for A,B being Element of Closed_Domains_of X holds(CLD-Union X).(A,B) = (D-Union X).(A,B);

theorem :: TDLAT_1:33
for A,B being Element of Closed_Domains_of X holds(CLD-Meet X).(A,B) = (D-Meet X).(A,B);

theorem :: TDLAT_1:36
for A,B being Element of Open_Domains_of X holds(OPD-Union X).(A,B) = (D-Union X).(A,B);

theorem :: TDLAT_1:37
for A,B being Element of Open_Domains_of X holds(OPD-Meet X).(A,B) = (D-Meet X).(A,B);

These properties have been reformulated as follows.
theorem :: TDLAT_1:39
CLD-Union X = (D-Union X)|[:Closed_Domains_of X,Closed_Domains_of X:];27

theorem :: TDLAT_1:40
CLD-Meet X = (D-Meet X)|[:Closed_Domains_of X,Closed_Domains_of X:];

theorem :: TDLAT_1:42
OPD-Union X = (D-Union X)|[:Open_Domains_of X,Open_Domains_of X:];

theorem :: TDLAT_1:43
OPD-Meet X = (D-Meet X)|[:Open_Domains_of X,Open_Domains_of X:];

Thus according to the de nition of sublattices, given at the end of subsection 4.1, we
can get immediately the following theorems (see [23]).
theorem :: TDLAT_1:41
Closed_Domains_Lattice X is SubLattice of Domains_Lattice X;

theorem :: TDLAT_1:44
Open_Domains_Lattice X is SubLattice of Domains_Lattice X;

5.4 Completeness of the lattices of domains

In [12], it is proved that the lattice of all domains of a given topological space is complete.
First, the following theorem has been formulated. We give also the skeleton of the Mizar
proof of it.
theorem :: TDLAT 2:90
for F being Subset of Domains Lattice X
ex a being Element of Domains Lattice X st F is less than a &for b being Element of Domains Lattice X st F is less than b holds a  b;
proof
let G be Subset of Domains Lattice X;G
the carrier of Domains Lattice X by AXIOMS:2;
then INC: G
Domains of X by TDLAT 2:86;
then reconsider F = G as Subset-Family of X by TOPS 2:3;
set A = (union F)(Int Cl(union F));F is domains-family by INC,TDLAT 2:65;
then A is domain by TDLAT 2:68;
then A
C where C is Subset of X : C is domain ;then A
Domains of X by TDLAT 1:def 1;
then Athe carrier of Domains Lattice X by TDLAT 2:86;
then reconsider a = A as Element of Domains Lattice X;





[

2f
2
2

g

28

take a;
LS: G is less than a@proofend;
for b being Element of Domains Lattice X st G is less than b holds a  b@proofend;
hence thesis by LS;
end;

Next, according to the de nition of complete lattices, given in the subsection 4.3, fromthis theorem we can get immediately the following one (see [23]).
theorem :: TDLAT_2:91
Domains_Lattice X is complete;

In the same way the completeness of the lattices of closed domains and of open domains
has been proved (comp. [2], [16]).
theorem :: TDLAT 2:98
for F being Subset of Closed Domains Lattice X
ex a being Element of Closed Domains Lattice X st
F is less than a &for b being Element of Closed Domains Lattice X st
F is less than b holds a  b;theorem :: TDLAT 2:107
for F being Subset of Open Domains Lattice X
ex a being Element of Open Domains Lattice X st
F is less than a &for b being Element of Open Domains Lattice X st
F is less than b holds a  b;theorem :: TDLAT_2:99
Closed_Domains_Lattice X is complete;theorem :: TDLAT_2:108
Open_Domains_Lattice X is complete;

6 The lattice of domains of an extremally disconnectedspace
In [11], a condition whether the lattice of all domains of a given topological space is Boolean
has been done. Namely, the lattice of all domains of a topological space X is Boolean if andonly if X is extremally disconnected. The aim of this section is to present this result. We
start with the properties of the lattice of domains of extremally disconnected spaces.
29reserve X for extremally_disconnected TopSpace;

theorem :: TDLAT_3:41
Domains_of X = Closed_Domains_of X;

theorem :: TDLAT_3:42
D-Union X = CLD-Union X & D-Meet X = CLD-Meet X;

theorem :: TDLAT_3:43
Domains_Lattice X = Closed_Domains_Lattice X;

theorem :: TDLAT_3:44
Domains_of X = Open_Domains_of X;

theorem :: TDLAT_3:45
D-Union X = OPD-Union X & D-Meet X = OPD-Meet X;

theorem :: TDLAT_3:46
Domains_Lattice X = Open_Domains_Lattice X;

theorem :: TDLAT 3:47
for A, B being Element of Domains of X holds(D-Union X).(A,B) = A
B & (D-Meet X).(A,B) = A

[

\ B;

theorem :: TDLAT 3:48
for a, b being Element of Domains Lattice X
for A, B being Element of Domains of X st a = A & b = B holds
a b = A
B & a b = A B;

t

[

u

\

In [11] the following lattice-theoretic characterization of extremally disconnected spaces
has been obtained. It says that a topological space is extremally disconnected if and only if
its lattice of all domains is modular. We give below the Mizar proof of it.
reserve X for TopSpace;30

theorem :: TDLAT_3:51
X is extremally_disconnected iff Domains_Lattice X is M_Lattice;

proof
CAR: Domains Lattice X =LattStr  Domains of X,D-Union X,D-Meet X  by TDLAT 1:def 4;thus X is extremally_disconnected implies Domains_Lattice X is M_Lattice
proof
assume X is extremally_disconnected;
then Domains_Lattice X = Open_Domains_Lattice X by TDLAT_3:46;
then Domains_Lattice X is D_Lattice by LATTICES:def 14;
hence Domains_Lattice X is M_Lattice by LATTICES:35;
end;
assume MD: Domains_Lattice X is M_Lattice;assume not X is extremally_disconnected;
then consider D being Subset of X such that
DOM: D is_domain and NEQ: Int Cl D <> Cl Int D by TDLAT_3:36;
set A = Int Cl D, C = Cl Int D, B = C`;ODCD: A is_open_domain & C is_closed_domain by TDLAT_1:23,22;
then ACD: A is_domain & C is_domain by TOPS_1:106,107;B` is_closed_domain by ODCD,PRE_TOPC:20;
then B is_open_domain by TOPS_1:101;then B is_domain by TOPS_1:107;g

2f

then BE where E is Subset of X : E is domain ;then reconsider b = B
as Element of Domains Lattice X by CAR,TDLAT 1:def 1;657 : AE where E is Subset of X : E is domain by ACD;
then AD: A Domains of X by TDLAT 1:def 1;
reconsider a = A
as Element of Domains Lattice X by CAR,TDLAT 1:def 1, 657 ;
658 : CE where E is Subset of X : E is domain by ACD;
then CD: C Domains of X by TDLAT 1:def 1;
reconsider c = C

2f
2

g

2f
2

g

31

as Element of Domains Lattice X by CAR,TDLAT 1:def 1, 658 ;A
D & D
C by DOM,TOPS 1:def 6;then A
C by BOOLE:29;
then MODEQ: a  c by AD,CD,TDLAT 2:89;
ODE: A = Int Cl A by ODCD,TOPS 1:def 8;
EIN: B C = X by TOPS 1:12;
AEM: A
X = A
by PRE TOPC:11.= A by BOOLE:60;bc = Cl(Int(B C)) (B C) by CAR,TDLAT 2:87.= X by EIN,TOPS 1:4;
then LS: a (b c) = Int(Cl A)
A by CAR,TDLAT 2:87,AEM.= A by ODE,BOOLE:62;
CDE: C = Cl Int C by ODCD,TOPS 1:def 7;
TR: B = Int (Int D)` by TDLAT 3:4.= Int Cl D` by TDLAT 3:3;
CDCL: Cl D is closed by PCOMPS 1:4;
Cl(A B) = Cl A
Cl B by PRE TOPC:50.= Cl Int(Cl D Cl D`) by TR,CDCL,TDLAT 1:6.= Cl Int Cl(D D`) by PRE TOPC:50.= Cl Int Cl X by TOPS 1:11.= Cl Int X by TOPS 1:27.= Cl X by TOPS 1:43.= X by TOPS 1:27;
then ab = Int( X) (AB) by CAR,TDLAT 2:87.= X
(AB) by TOPS 1:43.= X by TOPS 1:2;
then (ab)
c = Cl(Int( X C)) ( X C) by CAR,TDLAT 2:87.= Cl(Int C)( XC) by TOPS 1:3.= Cl(Int C)
C by TOPS 1:3.= C by CDE,BOOLE:65;
hence contradiction by NEQ,LS,MODEQ,MD,LATTICES:def 6;
end;







\ ;
[;
[;

u

;

\

t

\

u

[

[

[

t

t

\

[

u

[
[

[
[

[

\
\
\

\
\

\

From this theorem it follows the other lattice-theoretic characterization of extremallydisconnected spaces (comp. [11]). Namely, a topological space is extremally disconnected
if and only if its lattice of all domains is Boolean. We give also the Mizar proof of thistheorem.
theorem :: TDLAT_3:55
X is extremally_disconnected iff Domains_Lattice X is B_Lattice;

proof
thus X is extremally_disconnected implies Domains_Lattice X is B_Lattice
proof
assume X is extremally_disconnected;
then Domains_Lattice X = Open_Domains_Lattice X by TDLAT_3:46;

32

hence thesis;
end;assume Domains_Lattice X is B_Lattice;then Domains_Lattice X is D_Lattice by LATTICES:def 14;
then Domains_Lattice X is M_Lattice by LATTICES:35;
hence X is extremally_disconnected by TDLAT_3:51;
end;

Remarks. Because of the clustering constructions in Mizar, the following (true) sentence
requires a single direct justi cation only by the theorem given above.
for X being discrete TopSpace holds
Domains_Lattice X is Boolean Lattice by TDLAT_3:55;

But the following Mizar sentence is incorrect.
for X being almost_discrete TopStruct holds
Domains_Lattice X is modular by TDLAT_3:51;
::>

*103

The Mizar analyzer reports an error 103: Unknown functor.

Acknowledgments
The author would like to thank to Professor Andrzej Trybulec for many helpful conversations
during the preparation of this paper. The author is also very grateful to Czeslaw Bylinski
and Grzegorz Bancerek for useful suggestions.

References[1] G.Bancerek, Complete lattices, Formalized Math., 2 (1991), 719{725, MML: LATTICE3.
[2] G.Birkho , Lattice Theory, Providence., Rhode Island, New York, 1967.
[3] E. Bonarska, An Introduction to PC Mizar, Mizar Users Group. Foundation Philippele Hodey., Brussels, 1990.
[4] S. Burris and H. P.Sankappanavar, A Course in Universal Algebra, Springer-Verlag.,
New York, 1981.
33

[5] M. Chmur, The lattice of natural numbers and the sublattice of it. The set of prime
numbers, Formalized Math., 2 (1991), 453{459, MML: NAT LAT.
[6] A. Darmochwal and B. Padlewska, Topological spaces and continuous functions, Formalized Math., 1 (1990), 223{230, MML: PRE TOPC.
[7] A. Darmochwal and M. Wysocki, Subset of topological spaces, Formalized Math., 1(1990), 231{237, MML: TOPS 1.
[8] R. Engelking, General Topology, Monogra e Matematyczne Vol.60, PWN - Polish Scienti c Publishers, Warsaw 1977.
[9] G.Gratzer, General Lattice Theory, Akademie - Verlag., Berlin 1978.
[10] Y. Isomichi, New concepts in the theory of topological space - supercondensed set, subcondensed set, and condensed set, Paci c Journal of Math., 38 (1971), 657{668.
[11] Z. Karno, The lattice of domains of an extremally disconnected space, Formalized
Math., 3 (1992), MML: TDLAT 3.
[12] Z. Karno and T. Watanabe, Completeness of the lattice of domains of a topologicalspace, Formalized Math., 3 (1992), 71{79, MML: TDLAT 2.
[13] K. Kuratowski, Topology, Vol. I, PWN - Polish Scienti c Publishers and Academic
Press., Warsaw, New York and London, 1966.
[14] K. Kuratowski, Topology, Vol. II, PWN - Polish Scienti c Publishers and Academic
Press., Warsaw, New York and London, 1968.
[15] K. Kuratowski, Sur l'operation A de l'Analysis Situs, Fundamenta Math., 3 (1922),
182{199., (Selected Papers, PWN { Polish Scienti c Publishers., Warsaw 1988, pp.
95{112).
[16] K. Kuratowski and A. Mostowski, Set Theory (with an introduction to descriptive set
theory), Studies in Logic and The Foundations of Mathematics Vol.86, PWN - Polish
Scienti c Publishers and North-Holland Publishing Company., Warsaw-Amsterdam,
1976.
[17] H. MacNeille, Partially ordered sets, Trans. Amer. Math. Soc., 42 (1937), 416{460.
[18] P.Rudnicki, An overview of the Mizar project, Proceedings of the 1992 Workshop on
Types for Proofs and Programs, Eds. B. Nordstrom, K.Petersson and G.Plotkin, pp.
311{332.
[19] M. H. Stone, Application of the theory of Boolean rings to General Topology, Trans.
Amer. Math. Soc., 41 (1937), 375{481.
[20] M. H. Stone, Algebraic characterizations of special Boolean rings, Fundamenta Math.,
29 (1937), 223{303.
 additive und multiplikative Mengenkorper und Mengenfunktionen,[21] A. Tarski, Uber
Comptes Rendus Soc. Sci. Letter. Varsovie, 30 (1937), 151{181., (Collected Papers,
Vol. 2, Birkhauser, Boston 1985, pp. 289{322).
[22] A. Trybulec, Some features of the Mizar language, (these proceedings).
[23] T. Watanabe, The lattice of domains of a topological space, Formalized Math., 3 (1992),
41{46, MML: TDLAT 1.
_[24] S. Zukowski,
Introduction to lattice theory, Formalized Math., 1 (1990), 215{222, MML:LATTICES.
34