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


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.

MML Identifier: FINSUB_1

The terminology and notation used in this paper have been introduced in the following articles [5] [2] [6] [4]

Contents (PDF format)


[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]