:: Definitions and Basic Properties of Boolean & Union of Many
:: Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received April 27, 1995
:: Copyright (c) 1995-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 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;