:: BORSUK_6 semantic presentation

scheme :: BORSUK_6:sch 1
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] )
proof end;

theorem Th1: :: BORSUK_6:1
the carrier of [:I[01] ,I[01] :] = [:[.0,1.],[.0,1.]:] by BORSUK_1:83, BORSUK_1:def 5;

theorem :: BORSUK_6:2
canceled;

theorem :: BORSUK_6:3
canceled;

theorem :: BORSUK_6:4
canceled;

theorem Th5: :: BORSUK_6:5
for a, b, x being real number st a <= x & x <= b holds
(x - a) / (b - a) in the carrier of (Closed-Interval-TSpace 0,1)
proof end;

theorem Th6: :: BORSUK_6:6
for x being Point of I[01] st x <= 1 / 2 holds
2 * x is Point of I[01]
proof end;

theorem Th7: :: BORSUK_6:7
for x being Point of I[01] st x >= 1 / 2 holds
(2 * x) - 1 is Point of I[01]
proof end;

theorem Th8: :: BORSUK_6:8
for p, q being Point of I[01] holds p * q is Point of I[01]
proof end;

theorem Th9: :: BORSUK_6:9
for x being Point of I[01] holds (1 / 2) * x is Point of I[01]
proof end;

theorem Th10: :: BORSUK_6:10
for x being Point of I[01] st x >= 1 / 2 holds
x - (1 / 4) is Point of I[01]
proof end;

theorem :: BORSUK_6:11
canceled;

theorem Th12: :: BORSUK_6:12
id I[01] is Path of 0[01] , 1[01]
proof end;

theorem Th13: :: BORSUK_6:13
for a, b, c, d being Point of I[01] st a <= b & c <= d holds
[:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01] ,I[01] :]
proof end;

theorem Th14: :: BORSUK_6:14
for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 <= (2 * (p `1 )) - 1 } & T = { p where p is Point of (TOP-REAL 2) : p `2 <= p `1 } holds
(AffineMap 1,0,(1 / 2),(1 / 2)) .: S = T
proof end;

theorem Th15: :: BORSUK_6:15
for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1 )) - 1 } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= p `1 } holds
(AffineMap 1,0,(1 / 2),(1 / 2)) .: S = T
proof end;

theorem Th16: :: BORSUK_6:16
for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1 )) } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= - (p `1 ) } holds
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: S = T
proof end;

theorem Th17: :: BORSUK_6:17
for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 <= 1 - (2 * (p `1 )) } & T = { p where p is Point of (TOP-REAL 2) : p `2 <= - (p `1 ) } holds
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: S = T
proof end;

theorem Th18: :: BORSUK_6:18
for T being non empty 1-sorted holds
( T is real-membered iff for x being Element of T holds x is real )
proof end;

registration
cluster non empty real-membered 1-sorted ;
existence
ex b1 being 1-sorted st
( not b1 is empty & b1 is real-membered )
proof end;
cluster non empty real-membered TopStruct ;
existence
ex b1 being TopSpace st
( not b1 is empty & b1 is real-membered )
proof end;
end;

registration
let T be real-membered 1-sorted ;
cluster -> real Element of the carrier of T;
coherence
for b1 being Element of T holds b1 is real ;
end;

registration
let T be real-membered TopStruct ;
cluster -> real-membered SubSpace of T;
coherence
for b1 being SubSpace of T holds b1 is real-membered
proof end;
end;

registration
let S, T be non empty real-membered TopSpace;
let p be Element of [:S,T:];
cluster p `1 -> real ;
coherence
p `1 is real
proof end;
cluster p `2 -> real ;
coherence
p `2 is real
proof end;
end;

registration
let T be non empty SubSpace of [:I[01] ,I[01] :];
let x be Point of T;
cluster x `1 -> real ;
coherence
x `1 is real
proof end;
cluster x `2 -> real ;
coherence
x `2 is real
proof end;
end;

registration
cluster R^1 -> real-membered ;
coherence
R^1 is real-membered
proof end;
end;

theorem Th19: :: BORSUK_6:19
{ p where p is Point of (TOP-REAL 2) : p `2 <= (2 * (p `1 )) - 1 } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th20: :: BORSUK_6:20
{ p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1 )) - 1 } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th21: :: BORSUK_6:21
{ p where p is Point of (TOP-REAL 2) : p `2 <= 1 - (2 * (p `1 )) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th22: :: BORSUK_6:22
{ p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1 )) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th23: :: BORSUK_6:23
{ p where p is Point of (TOP-REAL 2) : ( p `2 >= 1 - (2 * (p `1 )) & p `2 >= (2 * (p `1 )) - 1 ) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th24: :: BORSUK_6:24
ex f being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st
for x, y being Real holds f . [x,y] = <*x,y*>
proof end;

theorem Th25: :: BORSUK_6:25
{ p where p is Point of [:R^1 ,R^1 :] : p `2 <= 1 - (2 * (p `1 )) } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th26: :: BORSUK_6:26
{ p where p is Point of [:R^1 ,R^1 :] : p `2 <= (2 * (p `1 )) - 1 } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th27: :: BORSUK_6:27
{ p where p is Point of [:R^1 ,R^1 :] : ( p `2 >= 1 - (2 * (p `1 )) & p `2 >= (2 * (p `1 )) - 1 ) } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th28: :: BORSUK_6:28
{ p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th29: :: BORSUK_6:29
{ p where p is Point of [:I[01] ,I[01] :] : ( p `2 >= 1 - (2 * (p `1 )) & p `2 >= (2 * (p `1 )) - 1 ) } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th30: :: BORSUK_6:30
{ p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th31: :: BORSUK_6:31
for S, T being non empty TopSpace
for p being Point of [:S,T:] holds
( p `1 is Point of S & p `2 is Point of T )
proof end;

theorem Th32: :: BORSUK_6:32
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] :]
proof end;

theorem Th33: :: BORSUK_6:33
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.]:]
proof end;

registration
let T be TopStruct ;
cluster {} T -> compact ;
coherence
{} T is compact by COMPTS_1:9;
end;

registration
let T be TopStruct ;
cluster empty compact Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is empty & b1 is compact )
proof end;
end;

theorem Th34: :: BORSUK_6:34
for T being TopStruct holds {} is empty compact Subset of T
proof end;

theorem Th35: :: BORSUK_6:35
for T being TopStruct
for a, b being real number st a > b holds
[.a,b.] is empty compact Subset of T
proof end;

theorem :: BORSUK_6:36
for a, b, c, d being Point of I[01] holds [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :]
proof end;

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 :: BORSUK_6:def 2
(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: :: BORSUK_6:37
for a, b, c, d being real number st a < b & c < d holds
( (L[01] a,b,c,d) . a = c & (L[01] a,b,c,d) . b = d )
proof end;

theorem Th38: :: BORSUK_6:38
for a, b, c, d being real number st a < b & c <= d holds
L[01] a,b,c,d is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
proof end;

theorem Th39: :: BORSUK_6:39
for a, b, c, d being real number st a < b & c <= d holds
for x being real number st a <= x & x <= b holds
(L[01] a,b,c,d) . x = (((d - c) / (b - a)) * (x - a)) + c
proof end;

theorem Th40: :: BORSUK_6:40
for f1, f2 being Function of [:I[01] ,I[01] :],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01] ,I[01] :] holds (f1 . p) * (f2 . p) is Point of I[01] ) holds
ex g being Function of [:I[01] ,I[01] :],I[01] st
( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 ) & g is continuous )
proof end;

theorem Th41: :: BORSUK_6:41
for f1, f2 being Function of [:I[01] ,I[01] :],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01] ,I[01] :] holds (f1 . p) + (f2 . p) is Point of I[01] ) holds
ex g being Function of [:I[01] ,I[01] :],I[01] st
( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous )
proof end;

theorem :: BORSUK_6:42
for f1, f2 being Function of [:I[01] ,I[01] :],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01] ,I[01] :] holds (f1 . p) - (f2 . p) is Point of I[01] ) holds
ex g being Function of [:I[01] ,I[01] :],I[01] st
( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 - r2 ) & g is continuous )
proof end;

theorem Th43: :: BORSUK_6:43
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b st P is continuous holds
P * (L[01] (0,1 (#) ),((#) 0,1)) is continuous Function of I[01] ,T
proof end;

theorem Th44: :: BORSUK_6:44
for X being non empty TopStruct
for a, b being Point of X
for P being Path of a,b st P . 0 = a & P . 1 = b holds
( (P * (L[01] (0,1 (#) ),((#) 0,1))) . 0 = b & (P * (L[01] (0,1 (#) ),((#) 0,1))) . 1 = a )
proof end;

theorem Th45: :: BORSUK_6:45
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b st P is continuous & P . 0 = a & P . 1 = b holds
( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )
proof end;

definition
let T be non empty TopSpace;
let a, b be Point of T;
:: original: are_connected
redefine pred a,b are_connected ;
reflexivity
for a being Point of T holds a,a are_connected
proof end;
symmetry
for a, b being Point of T st a,b are_connected holds
b,a are_connected
proof end;
end;

theorem Th46: :: BORSUK_6:46
for T being non empty TopSpace
for a, b, c being Point of T st a,b are_connected & b,c are_connected holds
a,c are_connected
proof end;

theorem :: BORSUK_6:47
canceled;

theorem :: BORSUK_6:48
canceled;

theorem :: BORSUK_6:49
canceled;

theorem Th50: :: BORSUK_6:50
for T being non empty TopSpace
for a, b being Point of T st a,b are_connected holds
for A being Path of a,b holds A = - (- A)
proof end;

theorem :: BORSUK_6:51
for T being non empty arcwise_connected TopSpace
for a, b being Point of T
for A being Path of a,b holds A = - (- A)
proof end;

definition
let T be non empty arcwise_connected TopSpace;
let a, b, c be Point of T;
let P be Path of a,b;
let Q be Path of b,c;
canceled;
redefine func P + Q means :: BORSUK_6:def 4
for t being Point of I[01] holds
( ( t <= 1 / 2 implies it . t = P . (2 * t) ) & ( 1 / 2 <= t implies it . t = Q . ((2 * t) - 1) ) );
compatibility
for b1 being Path of a,c holds
( b1 = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) ) )
proof end;
end;

:: deftheorem BORSUK_6:def 3 :
canceled;

:: deftheorem defines + BORSUK_6:def 4 :
for T being non empty arcwise_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) ) ) );

definition
let T be non empty arcwise_connected TopSpace;
let a, b be Point of T;
let P be Path of a,b;
redefine func - P means :Def5: :: BORSUK_6:def 5
for t being Point of I[01] holds it . t = P . (1 - t);
compatibility
for b1 being Path of b,a holds
( b1 = - P iff for t being Point of I[01] holds b1 . t = P . (1 - t) )
proof end;
end;

:: deftheorem Def5 defines - BORSUK_6:def 5 :
for T being non empty arcwise_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) );

definition
let T be non empty TopSpace;
let a, b be Point of T;
let P be Path of a,b;
let f be continuous Function of I[01] ,I[01] ;
assume A1: ( f . 0 = 0 & f . 1 = 1 & a,b are_connected ) ;
func RePar P,f -> Path of a,b equals :Def6: :: BORSUK_6:def 6
P * f;
coherence
P * f is Path of a,b
proof end;
end;

:: 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 :: BORSUK_6:52
canceled;

theorem Th53: :: BORSUK_6:53
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