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

Received April 14, 1989

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;