begin
theorem
theorem
:: deftheorem PBOOLE:def 1 :
canceled;
:: deftheorem PBOOLE:def 2 :
canceled;
:: deftheorem PBOOLE:def 3 :
canceled;
scheme
KuratowskiFunction{
F1()
-> set ,
F2(
set )
-> set } :
provided
A1:
for
e being
set st
e in F1() holds
F2(
e)
<> {}
:: deftheorem Def4 defines in PBOOLE:def 4 :
for I being set
for X, Y being ManySortedSet of I holds
( X in Y iff for i being set st i in I holds
X . i in Y . i );
:: deftheorem Def5 defines c= PBOOLE:def 5 :
for I being set
for X, Y being ManySortedSet of I holds
( X c= Y iff for i being set st i in I holds
X . i c= Y . i );
theorem Th3:
definition
let I be
set ;
func [[0]] I -> ManySortedSet of
I equals
I --> {};
coherence
I --> {} is ManySortedSet of I
;
correctness
;
let X,
Y be
ManySortedSet of
I;
func X \/ Y -> ManySortedSet of
I means :
Def7:
for
i being
set st
i in I holds
it . i = (X . i) \/ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \/ (Y . i) ) holds
b1 = b2
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) \/ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) \/ (X . i)
;
func X /\ Y -> ManySortedSet of
I means :
Def8:
for
i being
set st
i in I holds
it . i = (X . i) /\ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) /\ (Y . i) ) holds
b1 = b2
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) /\ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) /\ (X . i)
;
func X \ Y -> ManySortedSet of
I means :
Def9:
for
i being
set st
i in I holds
it . i = (X . i) \ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \ (Y . i) ) holds
b1 = b2
pred X overlaps Y means :
Def10:
for
i being
set st
i in I holds
X . i meets Y . i;
symmetry
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i meets Y . i ) holds
for i being set st i in I holds
Y . i meets X . i
;
pred X misses Y means :
Def11:
for
i being
set st
i in I holds
X . i misses Y . i;
symmetry
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i misses Y . i ) holds
for i being set st i in I holds
Y . i misses X . i
;
end;
:: deftheorem defines [[0]] PBOOLE:def 6 :
for I being set holds [[0]] I = I --> {};
:: deftheorem Def7 defines \/ PBOOLE:def 7 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X \/ Y iff for i being set st i in I holds
b4 . i = (X . i) \/ (Y . i) );
:: deftheorem Def8 defines /\ PBOOLE:def 8 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X /\ Y iff for i being set st i in I holds
b4 . i = (X . i) /\ (Y . i) );
:: deftheorem Def9 defines \ PBOOLE:def 9 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = X \ Y iff for i being set st i in I holds
b4 . i = (X . i) \ (Y . i) );
:: deftheorem Def10 defines overlaps PBOOLE:def 10 :
for I being set
for X, Y being ManySortedSet of I holds
( X overlaps Y iff for i being set st i in I holds
X . i meets Y . i );
:: deftheorem Def11 defines misses PBOOLE:def 11 :
for I being set
for X, Y being ManySortedSet of I holds
( X misses Y iff for i being set st i in I holds
X . i misses Y . i );
:: deftheorem defines \+\ PBOOLE:def 12 :
for I being set
for X, Y being ManySortedSet of I holds X \+\ Y = (X \ Y) \/ (Y \ X);
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
begin
:: deftheorem Def13 defines = PBOOLE:def 13 :
for I being set
for X, Y being ManySortedSet of I holds
( X = Y iff ( X c= Y & Y c= X ) );
theorem
canceled;
theorem
canceled;
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th49:
theorem Th50:
theorem
theorem
theorem Th53:
theorem
theorem
theorem
theorem
begin
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem
theorem
theorem Th65:
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem
theorem Th78:
theorem Th79:
theorem
theorem Th81:
theorem
theorem Th83:
theorem Th84:
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem Th95:
theorem
theorem
theorem Th98:
theorem
theorem Th100:
theorem Th101:
theorem Th102:
theorem Th103:
theorem
theorem
begin
theorem
theorem
canceled;
theorem Th108:
theorem Th109:
theorem Th110:
theorem
theorem
theorem
theorem
theorem
theorem Th116:
theorem
canceled;
theorem Th118:
theorem
theorem
theorem Th121:
theorem
theorem
theorem
theorem
canceled;
theorem Th126:
theorem
theorem
theorem
begin
:: deftheorem Def14 defines [= PBOOLE:def 14 :
for I being set
for X, Y being ManySortedSet of I holds
( X [= Y iff for x being ManySortedSet of I st x in X holds
x in Y );
theorem
theorem
canceled;
theorem
begin
theorem
theorem
theorem
theorem Th136:
theorem
theorem
theorem Th139:
theorem
begin
:: deftheorem Def15 defines empty-yielding PBOOLE:def 15 :
for I being set
for X being ManySortedSet of I holds
( X is empty-yielding iff for i being set st i in I holds
X . i is empty );
:: deftheorem Def16 defines non-empty PBOOLE:def 16 :
for I being set
for X being ManySortedSet of I holds
( X is non-empty iff for i being set st i in I holds
not X . i is empty );
theorem
theorem
theorem Th143:
theorem Th144:
theorem
theorem
theorem Th147:
theorem
begin
scheme
MSSEx{
F1()
-> set ,
P1[
set ,
set ] } :
provided
A1:
for
i being
set st
i in F1() holds
ex
j being
set st
P1[
i,
j]
begin
theorem Th149:
theorem
theorem
:: deftheorem defines Element PBOOLE:def 17 :
for I being set
for B, b3 being ManySortedSet of I holds
( b3 is Element of B iff for i being set st i in I holds
b3 . i is Element of B . i );
begin
:: deftheorem Def18 defines ManySortedFunction PBOOLE:def 18 :
for I being set
for A, B, b4 being ManySortedSet of I holds
( b4 is ManySortedFunction of A,B iff for i being set st i in I holds
b4 . i is Function of (A . i),(B . i) );
:: deftheorem Def19 defines # PBOOLE:def 19 :
for I being set
for M being ManySortedSet of I
for b3 being ManySortedSet of I * holds
( b3 = M # iff for i being Element of I * holds b3 . i = product (M * i) );
:: deftheorem Def20 defines *--> PBOOLE:def 20 :
for a being set
for b2 being Function of NAT,({a} *) holds
( b2 = *--> a iff for n being Element of NAT holds b2 . n = n |-> a );
theorem Th152:
theorem
:: deftheorem defines [| PBOOLE:def 21 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = [|X,Y|] iff for i being set st i in I holds
b4 . i = [:(X . i),(Y . i):] );
:: deftheorem defines MSFuncs PBOOLE:def 22 :
for I being set
for X, Y, b4 being ManySortedSet of I holds
( b4 = MSFuncs (X,Y) iff for i being set st i in I holds
b4 . i = Funcs ((X . i),(Y . i)) );
:: deftheorem Def23 defines ManySortedSubset PBOOLE:def 23 :
for I being set
for M, b3 being ManySortedSet of I holds
( b3 is ManySortedSubset of M iff b3 c= M );
:: deftheorem Def24 defines ** PBOOLE:def 24 :
for F, G, b3 being Function-yielding Function holds
( b3 = G ** F iff ( dom b3 = (dom F) /\ (dom G) & ( for i being set st i in dom b3 holds
b3 . i = (G . i) * (F . i) ) ) );
:: deftheorem defines .:.: PBOOLE:def 25 :
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b4 being ManySortedSet of I holds
( b4 = F .:.: A iff for i being set st i in I holds
b4 . i = (F . i) .: (A . i) );
theorem
theorem Th155:
theorem
theorem
:: deftheorem defines down PBOOLE:def 26 :
for I being set
for f being V8() ManySortedSet of I
for M being b2 -compatible ManySortedSet of I holds down M = M;
theorem
theorem
theorem
theorem