:: Definitions and Basic Properties of Boolean & Union of Many :: Sorted Sets :: by Artur Korni{\l}owicz :: :: Received April 27, 1995 :: Copyright (c) 1995-2018 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 PBOOLE, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_0, FUNCT_4, FUNCOP_1, TARSKI, FUNCT_2, FINSET_1, SETLIM_2; notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FUNCT_4, FUNCOP_1, PBOOLE; constructors FUNCT_4, PBOOLE, FINSET_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, FUNCOP_1, PRE_CIRC; requirements SUBSET, BOOLE; begin :: Boolean of Many Sorted Sets reserve x, y for object, I for set, A, B, X, Y for ManySortedSet of I; definition let I, A; func bool A -> ManySortedSet of I means :: MBOOLEAN:def 1 for i be object st i in I holds it.i = bool (A.i); end; registration let I, A; cluster bool A -> non-empty; end; theorem :: MBOOLEAN:1 :: Tarski:6 X = bool Y iff for A holds A in X iff A c= Y; theorem :: MBOOLEAN:2 :: ZFMISC_1:1 bool EmptyMS I = I --> {{}}; theorem :: MBOOLEAN:3 for x being set holds bool (I --> x) = I --> bool x; theorem :: MBOOLEAN:4 :: ZFMISC_1:30 bool (I --> {x}) = I --> { {} , {x} }; theorem :: MBOOLEAN:5 :: ZFMISC_1:76 EmptyMS I c= A; theorem :: MBOOLEAN:6 :: ZFMISC_1:79 A c= B implies bool A c= bool B; theorem :: MBOOLEAN:7 :: ZFMISC_1:81 bool A (\/) bool B c= bool (A (\/) B); theorem :: MBOOLEAN:8 :: ZFMISC_1:82 bool A (\/) bool B = bool (A (\/) B) implies for i be set st i in I holds A.i,B.i are_c=-comparable; theorem :: MBOOLEAN:9 :: ZFMISC_1:83 bool (A (/\) B) = bool A (/\) bool B; theorem :: MBOOLEAN:10 :: ZFMISC_1:84 bool (A (\) B) c= (I --> {{}}) (\/) (bool A (\) bool B); theorem :: MBOOLEAN:11 X c= A (\) B iff X c= A & X misses B; theorem :: MBOOLEAN:12 :: ZFMISC_1:86 bool (A (\) B) (\/) bool (B (\) A) c= bool (A (\+\) B); theorem :: MBOOLEAN:13 :: ZFMISC_1:87 X c= A (\+\) B iff X c= A (\/) B & X misses A (/\) B; theorem :: MBOOLEAN:14 :: ZFMISC_1:89 X c= A or Y c= A implies X (/\) Y c= A; theorem :: MBOOLEAN:15 :: ZFMISC_1:90 X c= A implies X (\) Y c= A; theorem :: MBOOLEAN:16 :: ZFMISC_1:91 X c= A & Y c= A implies X (\+\) Y c= A; theorem :: MBOOLEAN:17 :: ZFMISC_1:105 [|X, Y|] c= bool bool (X (\/) Y); theorem :: MBOOLEAN:18 :: FIN_TOPO:4 X c= A iff X in bool A; theorem :: MBOOLEAN:19 :: FRAENKEL:5 (Funcs)(A,B) c= bool [|A, B|]; begin :: Union of Many Sorted Sets definition let I, A; func union A -> ManySortedSet of I means :: MBOOLEAN:def 2 for i be object st i in I holds it.i = union (A.i); end; registration let I; cluster union EmptyMS I -> empty-yielding; end; theorem :: MBOOLEAN:20 :: Tarski:def 4 A in union X iff ex Y st A in Y & Y in X; theorem :: MBOOLEAN:21 :: ZFMISC_1:2 union EmptyMS I = EmptyMS I; theorem :: MBOOLEAN:22 for x being set holds union (I --> x) = I --> union x; theorem :: MBOOLEAN:23 :: ZFMISC_1:31 union (I --> {x}) = I --> x; theorem :: MBOOLEAN:24 :: ZFMISC_1:32 union (I --> { {x},{y} }) = I --> {x,y}; theorem :: MBOOLEAN:25 :: ZFMISC_1:92 X in A implies X c= union A; theorem :: MBOOLEAN:26 :: ZFMISC_1:95 A c= B implies union A c= union B; theorem :: MBOOLEAN:27 :: ZFMISC_1:96 union (A (\/) B) = union A (\/) union B; theorem :: MBOOLEAN:28 :: ZFMISC_1:97 union (A (/\) B) c= union A (/\) union B; theorem :: MBOOLEAN:29 :: ZFMISC_1:99 union bool A = A; theorem :: MBOOLEAN:30 :: ZFMISC_1:100 A c= bool union A; theorem :: MBOOLEAN:31 :: LATTICE4:1 union Y c= A & X in Y implies X c= A; theorem :: MBOOLEAN:32 :: ZFMISC_1:94 for Z be ManySortedSet of I for A be non-empty ManySortedSet of I holds (for X be ManySortedSet of I st X in A holds X c= Z) implies union A c= Z ; theorem :: MBOOLEAN:33 :: ZFMISC_1:98 for B be ManySortedSet of I for A be non-empty ManySortedSet of I st for X be ManySortedSet of I st X in A holds X (/\) B = EmptyMS I holds union(A) (/\) B = EmptyMS I; theorem :: MBOOLEAN:34 :: ZFMISC_1:101 for A, B be ManySortedSet of I st A (\/) B is non-empty & for X, Y be ManySortedSet of I st X <> Y & X in A (\/) B & Y in A (\/) B holds X (/\) Y = EmptyMS I holds union(A (/\) B) = union A (/\) union B; theorem :: MBOOLEAN:35 :: LOPCLSET:31 for A, X be ManySortedSet of I for B be non-empty ManySortedSet of I holds (X c= union (A (\/) B) & for Y be ManySortedSet of I st Y in B holds Y (/\) X = EmptyMS I) implies X c= union A; theorem :: MBOOLEAN:36 :: RLVECT_3:34 for A be finite-yielding non-empty ManySortedSet of I st (for X, Y be ManySortedSet of I st X in A & Y in A holds X c= Y or Y c= X) holds union A in A;