:: Boolean Domains
:: by Andrzej Trybulec and Agata Darmochwa\l
::
:: Received April 14, 1989
:: Copyright (c) 1990-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI, FINSET_1, FINSUB_1,
MATRIX_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1;
constructors TARSKI, SUBSET_1, FINSET_1;
registrations XBOOLE_0, SUBSET_1, FINSET_1;
requirements SUBSET, BOOLE;
begin :: Auxiliary theorems
reserve X,Y,x 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;
registration
cluster preBoolean -> cup-closed diff-closed for set;
cluster cup-closed diff-closed -> preBoolean for set;
end;
registration
cluster non empty cup-closed cap-closed diff-closed for set;
end;
theorem :: FINSUB_1:1
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;
reserve A for non empty preBoolean set;
definition
let A;
let X,Y be Element of A;
redefine func X \/ Y -> Element of A;
redefine func X \ Y -> Element of A;
end;
theorem :: FINSUB_1:2
X is Element of A & Y is Element of A implies X /\ Y is Element of A;
theorem :: FINSUB_1:3
X is Element of A & Y is Element of A implies X \+\ Y is Element of A;
theorem :: FINSUB_1:4
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:5
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:6
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;
redefine func X \+\ Y -> Element of A;
end;
theorem :: FINSUB_1:7
{} in A;
theorem :: FINSUB_1:8
for A being set holds bool A is preBoolean;
registration
let A be set;
cluster bool A -> preBoolean;
end;
theorem :: FINSUB_1:9
for A,B being non empty preBoolean set holds A /\ B is non empty preBoolean;
:: The set of all finite subsets of a set
definition
let A be set;
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;
registration
let A be set;
cluster Fin A -> non empty;
end;
registration
let A be set;
cluster -> finite for Element of Fin A;
end;
theorem :: FINSUB_1:10
for A, B being set st A c= B holds Fin A c= Fin B;
theorem :: FINSUB_1:11
for A, B being set holds Fin (A /\ B) = Fin A /\ Fin B;
theorem :: FINSUB_1:12
for A, B being set holds Fin A \/ Fin B c= Fin (A \/ B);
theorem :: FINSUB_1:13
for A being set holds Fin A c= bool A;
theorem :: FINSUB_1:14
for A being set st A is finite holds Fin A = bool A;
theorem :: FINSUB_1:15
Fin {} = { {} };
theorem :: FINSUB_1:16
for A being set, X being Element of Fin A holds X is Subset of A;
theorem :: FINSUB_1:17
for A being set, X being Subset of A st A is finite holds
X is Element of Fin A;