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

### Boolean Domains

by
Andrzej Trybulec, and
Agata Darmochwal

MML identifier: FINSUB_1
[ Mizar article, MML identifier index ]

```environ

vocabulary BOOLE, FINSET_1, FINSUB_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1;
constructors TARSKI, SUBSET_1, FINSET_1, XBOOLE_0;
clusters FINSET_1, SUBSET_1, XBOOLE_0, ZFMISC_1;
requirements SUBSET, BOOLE;

begin

:::::::::::::: Auxiliary theorems :::::::::::::::::::

reserve X,Y for set;

definition let IT be set;
attr IT is cup-closed means
:: FINSUB_1:def 1
for X,Y being set st X in IT & Y in IT holds X \/ Y in IT;
attr IT is cap-closed means
:: FINSUB_1:def 2
for X,Y being set st X in IT & Y in IT holds X /\ Y in IT;
attr IT is diff-closed means
:: FINSUB_1:def 3
for X,Y being set st X in IT & Y in IT holds X \ Y in IT;
end;

definition let IT be set;
attr IT is preBoolean means
:: FINSUB_1:def 4
IT is cup-closed diff-closed;
end;

definition
cluster preBoolean -> cup-closed diff-closed set;
cluster cup-closed diff-closed -> preBoolean set;
end;

definition
cluster non empty cup-closed cap-closed diff-closed set;
end;

reserve A for non empty preBoolean set;

canceled 9;

theorem :: FINSUB_1:10
for A being set holds A is preBoolean iff
for X,Y being set st X in A & Y in A holds X \/ Y in A & X \ Y in A;

definition let A; let X,Y be Element of A;
redefine func X \/ Y -> Element of A;
func X \ Y -> Element of A;
end;

canceled 2;

theorem :: FINSUB_1:13
X is Element of A & Y is Element of A implies X /\ Y is Element of A;

theorem :: FINSUB_1:14
X is Element of A & Y is Element of A implies X \+\ Y is Element of A;

theorem :: FINSUB_1:15
for A being non empty set st
for X,Y being Element of A holds X \+\ Y in A & X \ Y in A
holds A is preBoolean;

theorem :: FINSUB_1:16
for A being non empty set st
for X,Y being Element of A holds X \+\ Y in A & X /\ Y in A
holds A is preBoolean;

theorem :: FINSUB_1:17
for A being non empty set st
for X,Y being Element of A holds X \+\ Y in A & X \/ Y in A
holds A is preBoolean;

definition let A; let X,Y be Element of A;
redefine func X /\ Y -> Element of A;
func X \+\ Y -> Element of A;
end;

theorem :: FINSUB_1:18
{} in A;

canceled;

theorem :: FINSUB_1:20
for A being set holds bool A is preBoolean;

theorem :: FINSUB_1:21
for A,B being non empty preBoolean set holds A /\ B is non empty preBoolean;

reserve A,B,P for set;
reserve x for set;

:::::::::::::: The set of all finite subsets of a set ::::::::::::::::

definition let A;
func Fin A -> preBoolean set means
:: FINSUB_1:def 5
for X being set holds X in it iff X c= A & X is finite;
end;

definition let A;
cluster Fin A -> non empty;
end;

definition let A;
cluster -> finite Element of Fin A;
end;

canceled;

theorem :: FINSUB_1:23
A c= B implies Fin A c= Fin B;

theorem :: FINSUB_1:24
Fin (A /\ B) = Fin A /\ Fin B;

theorem :: FINSUB_1:25
Fin A \/ Fin B c= Fin (A \/ B);

theorem :: FINSUB_1:26
Fin A c= bool A;

theorem :: FINSUB_1:27
A is finite implies Fin A = bool A;

theorem :: FINSUB_1:28
Fin {} = { {} };

:::::::::::::: Finite subsets ::::::::::::::::

definition let A;
mode Finite_Subset of A is Element of Fin A;
end;

canceled;

theorem :: FINSUB_1:30
for X being Finite_Subset of A holds X is finite;

canceled;

theorem :: FINSUB_1:32
for X being Finite_Subset of A holds X is Subset of A;

canceled;

theorem :: FINSUB_1:34
A is finite implies
for X being Subset of A holds X is Finite_Subset of A;
```