begin
scheme
ExFunc3CondD{
F1()
-> non
empty set ,
P1[
set ],
P2[
set ],
P3[
set ],
F2(
set )
-> set ,
F3(
set )
-> set ,
F4(
set )
-> set } :
ex
f being
Function st
(
dom f = F1() & ( for
c being
Element of
F1() holds
( (
P1[
c] implies
f . c = F2(
c) ) & (
P2[
c] implies
f . c = F3(
c) ) & (
P3[
c] implies
f . c = F4(
c) ) ) ) )
provided
A1:
for
c being
Element of
F1() holds
( (
P1[
c] implies not
P2[
c] ) & (
P1[
c] implies not
P3[
c] ) & (
P2[
c] implies not
P3[
c] ) )
and A2:
for
c being
Element of
F1() holds
(
P1[
c] or
P2[
c] or
P3[
c] )
theorem Th1:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem Th13:
begin
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
begin
theorem Th18:
begin
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
for
A,
B being
Subset of st
A = [:[.0 ,(1 / 2).],[.0 ,1.]:] &
B = [:[.(1 / 2),1.],[.0 ,1.]:] holds
([#] ([:I[01] ,I[01] :] | A)) \/ ([#] ([:I[01] ,I[01] :] | B)) = [#] [:I[01] ,I[01] :]
theorem Th33:
for
A,
B being
Subset of st
A = [:[.0 ,(1 / 2).],[.0 ,1.]:] &
B = [:[.(1 / 2),1.],[.0 ,1.]:] holds
([#] ([:I[01] ,I[01] :] | A)) /\ ([#] ([:I[01] ,I[01] :] | B)) = [:{(1 / 2)},[.0 ,1.]:]
begin
theorem Th34:
theorem Th35:
theorem
begin
definition
let a,
b,
c,
d be
real number ;
canceled;func L[01] a,
b,
c,
d -> Function of
(Closed-Interval-TSpace a,b),
(Closed-Interval-TSpace c,d) equals
(L[01] ((#) c,d),(c,d (#) )) * (P[01] a,b,((#) 0 ,1),(0 ,1 (#) ));
correctness
coherence
(L[01] ((#) c,d),(c,d (#) )) * (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) is Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d);
;
end;
:: deftheorem BORSUK_6:def 1 :
canceled;
:: deftheorem defines L[01] BORSUK_6:def 2 :
for
a,
b,
c,
d being
real number holds
L[01] a,
b,
c,
d = (L[01] ((#) c,d),(c,d (#) )) * (P[01] a,b,((#) 0 ,1),(0 ,1 (#) ));
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
begin
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th50:
theorem
begin
:: deftheorem BORSUK_6:def 3 :
canceled;
:: deftheorem defines + BORSUK_6:def 4 :
:: deftheorem Def5 defines - BORSUK_6:def 5 :
begin
:: deftheorem Def6 defines RePar BORSUK_6:def 6 :
theorem
canceled;
theorem Th53:
theorem
:: deftheorem Def7 defines 1RP BORSUK_6:def 7 :
theorem Th55:
:: deftheorem Def8 defines 2RP BORSUK_6:def 8 :
theorem Th56:
:: deftheorem Def9 defines 3RP BORSUK_6:def 9 :
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
for
T being non
empty TopSpace for
a,
b,
c,
d being
Point of
for
P being
Path of
a,
b for
Q being
Path of
b,
c for
R being
Path of
c,
d st
a,
b are_connected &
b,
c are_connected &
c,
d are_connected holds
RePar ((P + Q) + R),
3RP = P + (Q + R)
begin
:: deftheorem Def10 defines LowerLeftUnitTriangle BORSUK_6:def 10 :
:: deftheorem Def11 defines UpperUnitTriangle BORSUK_6:def 11 :
:: deftheorem Def12 defines LowerRightUnitTriangle BORSUK_6:def 12 :
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
Lm1:
for x, y being Point of holds [x,y] in the carrier of [:I[01] ,I[01] :]
;
begin
theorem Th81:
for
T being non
empty TopSpace for
a,
b,
c,
d being
Point of
for
P being
Path of
a,
b for
Q being
Path of
b,
c for
R being
Path of
c,
d st
a,
b are_connected &
b,
c are_connected &
c,
d are_connected holds
(P + Q) + R,
P + (Q + R) are_homotopic
theorem
theorem Th83:
for
T being non
empty TopSpace for
a,
b,
c being
Point of
for
P1,
P2 being
Path of
a,
b for
Q1,
Q2 being
Path of
b,
c st
a,
b are_connected &
b,
c are_connected &
P1,
P2 are_homotopic &
Q1,
Q2 are_homotopic holds
P1 + Q1,
P2 + Q2 are_homotopic
theorem
theorem Th85:
theorem
theorem
theorem Th88:
theorem
theorem Th90:
theorem
theorem Th92:
theorem
theorem Th94:
theorem
theorem
definition
let T be non
empty TopSpace;
let a,
b be
Point of ;
let P,
Q be
Path of
a,
b;
assume A1:
P,
Q are_homotopic
;
mode Homotopy of
P,
Q -> Function of
[:I[01] ,I[01] :],
T means
(
it is
continuous & ( for
t being
Point of holds
(
it . t,
0 = P . t &
it . t,1
= Q . t &
it . 0 ,
t = a &
it . 1,
t = b ) ) );
existence
ex b1 being Function of [:I[01] ,I[01] :],T st
( b1 is continuous & ( for t being Point of holds
( b1 . t,0 = P . t & b1 . t,1 = Q . t & b1 . 0 ,t = a & b1 . 1,t = b ) ) )
by A1, BORSUK_2:def 7;
end;
:: deftheorem defines Homotopy BORSUK_6:def 13 :
for
T being non
empty TopSpace for
a,
b being
Point of
for
P,
Q being
Path of
a,
b st
P,
Q are_homotopic holds
for
b6 being
Function of
[:I[01] ,I[01] :],
T holds
(
b6 is
Homotopy of
P,
Q iff (
b6 is
continuous & ( for
t being
Point of holds
(
b6 . t,
0 = P . t &
b6 . t,1
= Q . t &
b6 . 0 ,
t = a &
b6 . 1,
t = b ) ) ) );