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

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.