Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Boolean Domains

Andrzej Trybulec

Warsaw University, Bialystok

Agata Darmochwal

Warsaw University, Bialystok
Summary.

BOOLE DOMAIN is a SET DOMAIN that is closed under union and difference.
This condition is equivalent to being closed under symmetric difference
and one of the following operations: union, intersection or difference.
We introduce the set of all finite subsets of a set $A$, denoted by Fin $A$.
The mode Finite Subset of a set $A$ is introduced with the mother type:
Element of Fin $A$.
In consequence,
``Finite Subset of \dots '' is an elementary type, therefore one may
use such types as ``set of Finite Subset of $A$'', ``[(Finite Subset of $A$),
Finite Subset of $A$]'', and so on.
The article begins with some auxiliary theorems that belong really
to [3] or [1] but are missing there.
Moreover, bool $A$ is redefined as a SET DOMAIN, for an arbitrary set $A$.
Supported by RPBP.III24.C1.
The terminology and notation used in this paper have been
introduced in the following articles
[5]
[2]
[6]
[4]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Library Committee.
Boolean properties of sets  requirements.
Journal of Formalized Mathematics,
EMM, 2002.
 [4]
Agata Darmochwal.
Finite sets.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [6]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received April 14, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]