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.III-24.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]