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
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
[:I[01],I[01]:] 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
[:I[01],I[01]:] 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 :
for T being non empty pathwise_connected TopSpace
for a, b, c being Point of T
for P being Path of a,b
for Q being Path of b,c
for b7 being Path of a,c holds
( b7 = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b7 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b7 . t = Q . ((2 * t) - 1) ) ) );
:: deftheorem Def5 defines - BORSUK_6:def 5 :
for T being non empty pathwise_connected TopSpace
for a, b being Point of T
for P being Path of a,b
for b5 being Path of b,a holds
( b5 = - P iff for t being Point of I[01] holds b5 . t = P . (1 - t) );
begin
:: deftheorem Def6 defines RePar BORSUK_6:def 6 :
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b
for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 & a,b are_connected holds
RePar (P,f) = P * f;
theorem
canceled;
theorem Th53:
theorem
:: deftheorem Def7 defines 1RP BORSUK_6:def 7 :
for b1 being Function of I[01],I[01] holds
( b1 = 1RP iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = 2 * t ) & ( t > 1 / 2 implies b1 . t = 1 ) ) );
theorem Th55:
:: deftheorem Def8 defines 2RP BORSUK_6:def 8 :
for b1 being Function of I[01],I[01] holds
( b1 = 2RP iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = 0 ) & ( t > 1 / 2 implies b1 . t = (2 * t) - 1 ) ) );
theorem Th56:
:: deftheorem Def9 defines 3RP BORSUK_6:def 9 :
for b1 being Function of I[01],I[01] holds
( b1 = 3RP iff for x being Point of I[01] holds
( ( x <= 1 / 2 implies b1 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b1 . x = x - (1 / 4) ) & ( x > 3 / 4 implies b1 . x = (2 * x) - 1 ) ) );
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
for
T being non
empty TopSpace for
a,
b,
c,
d being
Point of
T 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
definition
func LowerLeftUnitTriangle -> Subset of
[:I[01],I[01]:] means :
Def10:
for
x being
set holds
(
x in it iff ex
a,
b being
Point of
I[01] st
(
x = [a,b] &
b <= 1
- (2 * a) ) );
existence
ex b1 being Subset of [:I[01],I[01]:] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) )
uniqueness
for b1, b2 being Subset of [:I[01],I[01]:] st ( for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) ) ) holds
b1 = b2
end;
:: deftheorem Def10 defines LowerLeftUnitTriangle BORSUK_6:def 10 :
for b1 being Subset of [:I[01],I[01]:] holds
( b1 = LowerLeftUnitTriangle iff for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) ) );
definition
func UpperUnitTriangle -> Subset of
[:I[01],I[01]:] means :
Def11:
for
x being
set holds
(
x in it iff ex
a,
b being
Point of
I[01] st
(
x = [a,b] &
b >= 1
- (2 * a) &
b >= (2 * a) - 1 ) );
existence
ex b1 being Subset of [:I[01],I[01]:] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) )
uniqueness
for b1, b2 being Subset of [:I[01],I[01]:] st ( for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines UpperUnitTriangle BORSUK_6:def 11 :
for b1 being Subset of [:I[01],I[01]:] holds
( b1 = UpperUnitTriangle iff for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) );
definition
func LowerRightUnitTriangle -> Subset of
[:I[01],I[01]:] means :
Def12:
for
x being
set holds
(
x in it iff ex
a,
b being
Point of
I[01] st
(
x = [a,b] &
b <= (2 * a) - 1 ) );
existence
ex b1 being Subset of [:I[01],I[01]:] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) )
uniqueness
for b1, b2 being Subset of [:I[01],I[01]:] st ( for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) ) ) holds
b1 = b2
end;
:: deftheorem Def12 defines LowerRightUnitTriangle BORSUK_6:def 12 :
for b1 being Subset of [:I[01],I[01]:] holds
( b1 = LowerRightUnitTriangle iff for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) ) );
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 I[01] 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
T 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
T 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
T;
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
I[01] 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 I[01] 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 T
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 I[01] holds
( b6 . (t,0) = P . t & b6 . (t,1) = Q . t & b6 . (0,t) = a & b6 . (1,t) = b ) ) ) );