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.

#### 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)

#### 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.