:: Boolean Domains :: by Andrzej Trybulec and Agata Darmochwa\l :: :: Received April 14, 1989 :: Copyright (c) 1990-2021 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;