:: Algebraic Properties of Homotopies :: by Adam Grabowski and Artur Korni{\l}owicz :: :: Received March 18, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin 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] ) proofend; theorem Th1: :: BORSUK_6:1 the carrier of [:I[01],I[01]:] = [:[.0,1.],[.0,1.]:] by BORSUK_1:40, BORSUK_1:def_2; theorem Th2: :: BORSUK_6:2 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)) proofend; theorem Th3: :: BORSUK_6:3 for x being Point of I[01] st x <= 1 / 2 holds 2 * x is Point of I[01] proofend; theorem Th4: :: BORSUK_6:4 for x being Point of I[01] st x >= 1 / 2 holds (2 * x) - 1 is Point of I[01] proofend; theorem Th5: :: BORSUK_6:5 for p, q being Point of I[01] holds p * q is Point of I[01] proofend; theorem Th6: :: BORSUK_6:6 for x being Point of I[01] holds (1 / 2) * x is Point of I[01] proofend; theorem Th7: :: BORSUK_6:7 for x being Point of I[01] st x >= 1 / 2 holds x - (1 / 4) is Point of I[01] proofend; theorem Th8: :: BORSUK_6:8 id I[01] is Path of 0[01] , 1[01] proofend; theorem Th9: :: BORSUK_6:9 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]:] proofend; begin theorem Th10: :: BORSUK_6:10 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 proofend; theorem Th11: :: BORSUK_6:11 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 proofend; theorem Th12: :: BORSUK_6:12 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 proofend; theorem Th13: :: BORSUK_6:13 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 proofend; begin theorem :: BORSUK_6:14 for T being non empty 1-sorted holds ( T is real-membered iff for x being Element of T holds x is real ) proofend; registration cluster non empty real-membered for 1-sorted ; existence ex b1 being 1-sorted st ( not b1 is empty & b1 is real-membered ) proofend; cluster non empty TopSpace-like real-membered for TopStruct ; existence ex b1 being TopSpace st ( not b1 is empty & b1 is real-membered ) proofend; end; registration let T be real-membered 1-sorted ; cluster -> real for 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 for SubSpace of T; coherence for b1 being SubSpace of T holds b1 is real-membered ; end; registration let S, T be non empty real-membered TopSpace; let p be Element of [:S,T:]; clusterp `1 -> real ; coherence p `1 is real proofend; clusterp `2 -> real ; coherence p `2 is real proofend; end; registration let T be non empty SubSpace of [:I[01],I[01]:]; let x be Point of T; clusterx `1 -> real ; coherence x `1 is real proofend; clusterx `2 -> real ; coherence x `2 is real proofend; end; begin theorem Th15: :: BORSUK_6:15 { p where p is Point of (TOP-REAL 2) : p `2 <= (2 * (p `1)) - 1 } is closed Subset of (TOP-REAL 2) proofend; theorem Th16: :: BORSUK_6:16 { p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1)) - 1 } is closed Subset of (TOP-REAL 2) proofend; theorem Th17: :: BORSUK_6:17 { p where p is Point of (TOP-REAL 2) : p `2 <= 1 - (2 * (p `1)) } is closed Subset of (TOP-REAL 2) proofend; theorem Th18: :: BORSUK_6:18 { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1)) } is closed Subset of (TOP-REAL 2) proofend; theorem Th19: :: BORSUK_6:19 { 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) proofend; theorem Th20: :: BORSUK_6:20 ex f being Function of [:R^1,R^1:],(TOP-REAL 2) st for x, y being Real holds f . [x,y] = <*x,y*> proofend; theorem Th21: :: BORSUK_6:21 { p where p is Point of [:R^1,R^1:] : p `2 <= 1 - (2 * (p `1)) } is closed Subset of [:R^1,R^1:] proofend; theorem Th22: :: BORSUK_6:22 { p where p is Point of [:R^1,R^1:] : p `2 <= (2 * (p `1)) - 1 } is closed Subset of [:R^1,R^1:] proofend; theorem Th23: :: BORSUK_6:23 { 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:] proofend; theorem Th24: :: BORSUK_6:24 { 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]:] proofend; theorem Th25: :: BORSUK_6:25 { 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]:] proofend; theorem Th26: :: BORSUK_6:26 { 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]:] proofend; theorem Th27: :: BORSUK_6:27 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 ) proofend; theorem Th28: :: BORSUK_6:28 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]:] proofend; theorem Th29: :: BORSUK_6:29 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.]:] proofend; begin registration let T be TopStruct ; cluster empty compact for Element of bool the carrier of T; existence ex b1 being Subset of T st ( b1 is empty & b1 is compact ) proofend; end; theorem Th30: :: BORSUK_6:30 for T being TopStruct holds {} is empty compact Subset of T proofend; theorem Th31: :: BORSUK_6:31 for T being TopStruct for a, b being real number st a > b holds [.a,b.] is empty compact Subset of T proofend; theorem :: BORSUK_6:32 for a, b, c, d being Point of I[01] holds [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01],I[01]:] proofend; begin definition let a, b, c, d be real number ; func L[01] (a,b,c,d) -> Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) equals :: BORSUK_6:def 1 (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 defines L[01] BORSUK_6:def_1_:_ 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 Th33: :: BORSUK_6:33 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 ) proofend; theorem Th34: :: BORSUK_6:34 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)) proofend; theorem Th35: :: BORSUK_6:35 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 proofend; theorem Th36: :: BORSUK_6:36 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 ) proofend; theorem Th37: :: BORSUK_6:37 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 ) proofend; theorem :: BORSUK_6:38 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 ) proofend; begin theorem Th39: :: BORSUK_6:39 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 proofend; theorem Th40: :: BORSUK_6:40 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 ) proofend; theorem Th41: :: BORSUK_6:41 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 ) proofend; definition let T be non empty TopSpace; let a, b be Point of T; :: original:are_connected redefine preda,b are_connected ; reflexivity for a being Point of T holds R61(T,b1,b1) proofend; symmetry for a, b being Point of T st R61(T,b1,b2) holds R61(T,b2,b1) proofend; end; theorem Th42: :: BORSUK_6:42 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 proofend; theorem Th43: :: BORSUK_6:43 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) proofend; theorem :: BORSUK_6:44 for T being non empty pathwise_connected TopSpace for a, b being Point of T for A being Path of a,b holds A = - (- A) proofend; begin definition let T be non empty pathwise_connected TopSpace; let a, b, c be Point of T; let P be Path of a,b; let Q be Path of b,c; redefine func P + Q means :: BORSUK_6:def 2 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) ) ) ) proofend; end; :: deftheorem defines + BORSUK_6:def_2_:_ 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) ) ) ); definition let T be non empty pathwise_connected TopSpace; let a, b be Point of T; let P be Path of a,b; redefine func - P means :Def3: :: BORSUK_6:def 3 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) ) proofend; end; :: deftheorem Def3 defines - BORSUK_6:def_3_:_ 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 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 that A1: f . 0 = 0 and A2: f . 1 = 1 and A3: a,b are_connected ; func RePar (P,f) -> Path of a,b equals :Def4: :: BORSUK_6:def 4 P * f; coherence P * f is Path of a,b proofend; end; :: deftheorem Def4 defines RePar BORSUK_6:def_4_:_ 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 Th45: :: BORSUK_6:45 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 are_homotopic proofend; theorem :: BORSUK_6:46 for T being non empty pathwise_connected 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 holds RePar (P,f),P are_homotopic proofend; definition func 1RP -> Function of I[01],I[01] means :Def5: :: BORSUK_6:def 5 for t being Point of I[01] holds ( ( t <= 1 / 2 implies it . t = 2 * t ) & ( t > 1 / 2 implies it . t = 1 ) ); existence ex b1 being Function of I[01],I[01] st for t being Point of I[01] holds ( ( t <= 1 / 2 implies b1 . t = 2 * t ) & ( t > 1 / 2 implies b1 . t = 1 ) ) proofend; uniqueness for b1, b2 being Function of I[01],I[01] st ( for t being Point of I[01] holds ( ( t <= 1 / 2 implies b1 . t = 2 * t ) & ( t > 1 / 2 implies b1 . t = 1 ) ) ) & ( for t being Point of I[01] holds ( ( t <= 1 / 2 implies b2 . t = 2 * t ) & ( t > 1 / 2 implies b2 . t = 1 ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines 1RP BORSUK_6:def_5_:_ 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 ) ) ); registration cluster 1RP -> continuous ; coherence 1RP is continuous proofend; end; theorem Th47: :: BORSUK_6:47 ( 1RP . 0 = 0 & 1RP . 1 = 1 ) proofend; definition func 2RP -> Function of I[01],I[01] means :Def6: :: BORSUK_6:def 6 for t being Point of I[01] holds ( ( t <= 1 / 2 implies it . t = 0 ) & ( t > 1 / 2 implies it . t = (2 * t) - 1 ) ); existence ex b1 being Function of I[01],I[01] st for t being Point of I[01] holds ( ( t <= 1 / 2 implies b1 . t = 0 ) & ( t > 1 / 2 implies b1 . t = (2 * t) - 1 ) ) proofend; uniqueness for b1, b2 being Function of I[01],I[01] st ( for t being Point of I[01] holds ( ( t <= 1 / 2 implies b1 . t = 0 ) & ( t > 1 / 2 implies b1 . t = (2 * t) - 1 ) ) ) & ( for t being Point of I[01] holds ( ( t <= 1 / 2 implies b2 . t = 0 ) & ( t > 1 / 2 implies b2 . t = (2 * t) - 1 ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines 2RP BORSUK_6:def_6_:_ 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 ) ) ); registration cluster 2RP -> continuous ; coherence 2RP is continuous proofend; end; theorem Th48: :: BORSUK_6:48 ( 2RP . 0 = 0 & 2RP . 1 = 1 ) proofend; definition func 3RP -> Function of I[01],I[01] means :Def7: :: BORSUK_6:def 7 for x being Point of I[01] holds ( ( x <= 1 / 2 implies it . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies it . x = x - (1 / 4) ) & ( x > 3 / 4 implies it . x = (2 * x) - 1 ) ); existence ex b1 being Function of I[01],I[01] st 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 ) ) proofend; uniqueness for b1, b2 being Function of I[01],I[01] st ( 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 ) ) ) & ( for x being Point of I[01] holds ( ( x <= 1 / 2 implies b2 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b2 . x = x - (1 / 4) ) & ( x > 3 / 4 implies b2 . x = (2 * x) - 1 ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines 3RP BORSUK_6:def_7_:_ 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 ) ) ); registration cluster 3RP -> continuous ; coherence 3RP is continuous proofend; end; theorem Th49: :: BORSUK_6:49 ( 3RP . 0 = 0 & 3RP . 1 = 1 ) proofend; theorem Th50: :: BORSUK_6:50 for T being non empty TopSpace for a, b being Point of T for P being Path of a,b for Q being constant Path of b,b st a,b are_connected holds RePar (P,1RP) = P + Q proofend; theorem Th51: :: BORSUK_6:51 for T being non empty TopSpace for a, b being Point of T for P being Path of a,b for Q being constant Path of a,a st a,b are_connected holds RePar (P,2RP) = Q + P proofend; theorem Th52: :: BORSUK_6:52 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) proofend; begin definition func LowerLeftUnitTriangle -> Subset of [:I[01],I[01]:] means :Def8: :: BORSUK_6:def 8 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) ) ) proofend; 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 proofend; end; :: deftheorem Def8 defines LowerLeftUnitTriangle BORSUK_6:def_8_:_ 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) ) ) ); notation synonym IAA for LowerLeftUnitTriangle ; end; definition func UpperUnitTriangle -> Subset of [:I[01],I[01]:] means :Def9: :: BORSUK_6:def 9 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 ) ) proofend; 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 proofend; end; :: deftheorem Def9 defines UpperUnitTriangle BORSUK_6:def_9_:_ 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 ) ) ); notation synonym IBB for UpperUnitTriangle ; end; definition func LowerRightUnitTriangle -> Subset of [:I[01],I[01]:] means :Def10: :: BORSUK_6:def 10 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 ) ) proofend; 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 proofend; end; :: deftheorem Def10 defines LowerRightUnitTriangle BORSUK_6:def_10_:_ 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 ) ) ); notation synonym ICC for LowerRightUnitTriangle ; end; theorem Th53: :: BORSUK_6:53 IAA = { p where p is Point of [:I[01],I[01]:] : p `2 <= 1 - (2 * (p `1)) } proofend; theorem Th54: :: BORSUK_6:54 IBB = { p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } proofend; theorem Th55: :: BORSUK_6:55 ICC = { p where p is Point of [:I[01],I[01]:] : p `2 <= (2 * (p `1)) - 1 } proofend; registration cluster LowerLeftUnitTriangle -> non empty closed ; coherence ( IAA is closed & not IAA is empty ) by Th24, Th53; cluster UpperUnitTriangle -> non empty closed ; coherence ( IBB is closed & not IBB is empty ) by Th25, Th54; cluster LowerRightUnitTriangle -> non empty closed ; coherence ( ICC is closed & not ICC is empty ) by Th26, Th55; end; theorem Th56: :: BORSUK_6:56 (IAA \/ IBB) \/ ICC = [:[.0,1.],[.0,1.]:] proofend; theorem Th57: :: BORSUK_6:57 IAA /\ IBB = { p where p is Point of [:I[01],I[01]:] : p `2 = 1 - (2 * (p `1)) } proofend; theorem Th58: :: BORSUK_6:58 ICC /\ IBB = { p where p is Point of [:I[01],I[01]:] : p `2 = (2 * (p `1)) - 1 } proofend; theorem Th59: :: BORSUK_6:59 for x being Point of [:I[01],I[01]:] st x in IAA holds x `1 <= 1 / 2 proofend; theorem Th60: :: BORSUK_6:60 for x being Point of [:I[01],I[01]:] st x in ICC holds x `1 >= 1 / 2 proofend; theorem Th61: :: BORSUK_6:61 for x being Point of I[01] holds [0,x] in IAA proofend; theorem Th62: :: BORSUK_6:62 for s being set st [0,s] in IBB holds s = 1 proofend; theorem Th63: :: BORSUK_6:63 for s being set st [s,1] in ICC holds s = 1 proofend; theorem Th64: :: BORSUK_6:64 [0,1] in IBB proofend; theorem Th65: :: BORSUK_6:65 for x being Point of I[01] holds [x,1] in IBB proofend; theorem Th66: :: BORSUK_6:66 ( [(1 / 2),0] in ICC & [1,1] in ICC ) proofend; theorem Th67: :: BORSUK_6:67 [(1 / 2),0] in IBB proofend; theorem Th68: :: BORSUK_6:68 for x being Point of I[01] holds [1,x] in ICC proofend; theorem Th69: :: BORSUK_6:69 for x being Point of I[01] st x >= 1 / 2 holds [x,0] in ICC proofend; theorem Th70: :: BORSUK_6:70 for x being Point of I[01] st x <= 1 / 2 holds [x,0] in IAA proofend; theorem Th71: :: BORSUK_6:71 for x being Point of I[01] st x < 1 / 2 holds ( not [x,0] in IBB & not [x,0] in ICC ) proofend; theorem Th72: :: BORSUK_6:72 IAA /\ ICC = {[(1 / 2),0]} proofend; Lm1: for x, y being Point of I[01] holds [x,y] in the carrier of [:I[01],I[01]:] ; begin theorem Th73: :: BORSUK_6:73 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 proofend; theorem :: BORSUK_6:74 for X being non empty pathwise_connected TopSpace for a1, b1, c1, d1 being Point of X for P being Path of a1,b1 for Q being Path of b1,c1 for R being Path of c1,d1 holds (P + Q) + R,P + (Q + R) are_homotopic proofend; theorem Th75: :: BORSUK_6:75 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 proofend; theorem :: BORSUK_6:76 for X being non empty pathwise_connected TopSpace for a1, b1, c1 being Point of X for P1, P2 being Path of a1,b1 for Q1, Q2 being Path of b1,c1 st P1,P2 are_homotopic & Q1,Q2 are_homotopic holds P1 + Q1,P2 + Q2 are_homotopic proofend; theorem Th77: :: BORSUK_6:77 for T being non empty TopSpace for a, b being Point of T for P, Q being Path of a,b st a,b are_connected & P,Q are_homotopic holds - P, - Q are_homotopic proofend; theorem :: BORSUK_6:78 for X being non empty pathwise_connected TopSpace for a1, b1 being Point of X for P, Q being Path of a1,b1 st P,Q are_homotopic holds - P, - Q are_homotopic proofend; theorem :: BORSUK_6:79 for T being non empty TopSpace for a, b being Point of T for P, Q, R being Path of a,b st P,Q are_homotopic & Q,R are_homotopic holds P,R are_homotopic proofend; theorem Th80: :: BORSUK_6:80 for T being non empty TopSpace for a, b being Point of T for P being Path of a,b for Q being constant Path of b,b st a,b are_connected holds P + Q,P are_homotopic proofend; theorem :: BORSUK_6:81 for X being non empty pathwise_connected TopSpace for a1, b1 being Point of X for P being Path of a1,b1 for Q being constant Path of b1,b1 holds P + Q,P are_homotopic proofend; theorem Th82: :: BORSUK_6:82 for T being non empty TopSpace for a, b being Point of T for P being Path of a,b for Q being constant Path of a,a st a,b are_connected holds Q + P,P are_homotopic proofend; theorem :: BORSUK_6:83 for X being non empty pathwise_connected TopSpace for a1, b1 being Point of X for P being Path of a1,b1 for Q being constant Path of a1,a1 holds Q + P,P are_homotopic proofend; theorem Th84: :: BORSUK_6:84 for T being non empty TopSpace for a, b being Point of T for P being Path of a,b for Q being constant Path of a,a st a,b are_connected holds P + (- P),Q are_homotopic proofend; theorem :: BORSUK_6:85 for X being non empty pathwise_connected TopSpace for a1, b1 being Point of X for P being Path of a1,b1 for Q being constant Path of a1,a1 holds P + (- P),Q are_homotopic proofend; theorem Th86: :: BORSUK_6:86 for T being non empty TopSpace for b, a being Point of T for P being Path of b,a for Q being constant Path of a,a st b,a are_connected holds (- P) + P,Q are_homotopic proofend; theorem :: BORSUK_6:87 for X being non empty pathwise_connected TopSpace for b1, a1 being Point of X for P being Path of b1,a1 for Q being constant Path of a1,a1 holds (- P) + P,Q are_homotopic proofend; theorem :: BORSUK_6:88 for T being non empty TopSpace for a being Point of T for P, Q being constant Path of a,a holds P,Q are_homotopic proofend; 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 :: BORSUK_6:def 11 ( 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_11_:_ 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 ) ) ) );