:: The {B}orsuk-Ulam Theorem :: by Artur Korni{\l}owicz and Marco Riccardi :: :: Received November 3, 2011 :: Copyright (c) 2011-2012 Association of Mizar Users begin reconsider Q = 0 as Nat ; set T2 = TOP-REAL 2; set o2 = |[0,0]|; set o = |[0,0,0]|; set I = the carrier of I[01]; set II = the carrier of [:I[01],I[01]:]; set R = the carrier of R^1; set X01 = [.0,1.[; set K = R^1 [.0,1.[; set R01 = R^1 | (R^1 ].0,1.[); reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15; Lm1: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2; Lm2: 0 in {0} by TARSKI:def_1; Lm3: now__::_thesis:_for_s_being_real_number_st_s_<=_1_/_2_&_0_<=_s_holds_ s_in_the_carrier_of_I[01] let s be real number ; ::_thesis: ( s <= 1 / 2 & 0 <= s implies s in the carrier of I[01] ) assume s <= 1 / 2 ; ::_thesis: ( 0 <= s implies s in the carrier of I[01] ) then s <= 1 by XXREAL_0:2; hence ( 0 <= s implies s in the carrier of I[01] ) by BORSUK_1:43; ::_thesis: verum end; Lm4: now__::_thesis:_for_s_being_real_number_st_0_<=_s_&_s_<=_1_/_2_holds_ s_+_(1_/_2)_in_the_carrier_of_I[01] let s be real number ; ::_thesis: ( 0 <= s & s <= 1 / 2 implies s + (1 / 2) in the carrier of I[01] ) set t = s + (1 / 2); assume ( 0 <= s & s <= 1 / 2 ) ; ::_thesis: s + (1 / 2) in the carrier of I[01] then ( Q + (1 / 2) <= s + (1 / 2) & s + (1 / 2) <= (1 / 2) + (1 / 2) ) by XREAL_1:6; hence s + (1 / 2) in the carrier of I[01] by BORSUK_1:43; ::_thesis: verum end; registration cluster -> irrational for Element of IRRAT ; coherence for b1 being Element of IRRAT holds b1 is irrational by BORSUK_5:17; end; theorem Th1: :: BORSUK_7:1 for r, s being real number st 0 <= r & 0 <= s & r ^2 = s ^2 holds r = s proofend; theorem Th2: :: BORSUK_7:2 for r, s being real number st frac r >= frac s holds frac (r - s) = (frac r) - (frac s) proofend; theorem Th3: :: BORSUK_7:3 for r, s being real number st frac r < frac s holds frac (r - s) = ((frac r) - (frac s)) + 1 proofend; theorem Th4: :: BORSUK_7:4 for r, s being real number ex i being Integer st ( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) ) proofend; theorem Th5: :: BORSUK_7:5 for r being real number holds ( not sin r = 0 or r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) proofend; theorem Th6: :: BORSUK_7:6 for r being real number holds ( not cos r = 0 or r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) ) proofend; theorem Th7: :: BORSUK_7:7 for r being real number st sin r = 0 holds ex i being Integer st r = PI * i proofend; theorem Th8: :: BORSUK_7:8 for r being real number st cos r = 0 holds ex i being Integer st r = (PI / 2) + (PI * i) proofend; Lm5: now__::_thesis:_for_r,_s_being_real_number_st_sin_((r_-_s)_/_2)_=_0_holds_ ex_i_being_Integer_st_r_=_s_+_((2_*_PI)_*_i) let r, s be real number ; ::_thesis: ( sin ((r - s) / 2) = 0 implies ex i being Integer st r = s + ((2 * PI) * i) ) assume sin ((r - s) / 2) = 0 ; ::_thesis: ex i being Integer st r = s + ((2 * PI) * i) then consider i being Integer such that A1: (r - s) / 2 = PI * i by Th7; r = s + ((2 * PI) * i) by A1; hence ex i being Integer st r = s + ((2 * PI) * i) ; ::_thesis: verum end; theorem Th9: :: BORSUK_7:9 for r, s being real number st sin r = sin s holds ex i being Integer st ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) proofend; theorem Th10: :: BORSUK_7:10 for r, s being real number st cos r = cos s holds ex i being Integer st ( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) proofend; theorem Th11: :: BORSUK_7:11 for r, s being real number st sin r = sin s & cos r = cos s holds ex i being Integer st r = s + ((2 * PI) * i) proofend; theorem Th12: :: BORSUK_7:12 for i being Integer for c1, c2 being complex number st |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) holds c1 = c2 proofend; registration let f be one-to-one complex-valued Function; let c be complex number ; clusterc + f -> one-to-one ; coherence f + c is one-to-one proofend; end; registration let f be one-to-one complex-valued Function; let c be complex number ; clusterf - c -> one-to-one ; coherence f - c is one-to-one ; end; theorem Th13: :: BORSUK_7:13 for f being complex-valued FinSequence holds len (- f) = len f proofend; theorem Th14: :: BORSUK_7:14 for n being Nat holds - (0* n) = 0* n proofend; theorem Th15: :: BORSUK_7:15 for n being Nat for f being complex-valued Function st f <> 0* n holds - f <> 0* n proofend; theorem Th16: :: BORSUK_7:16 for r1, r2, r3 being real number holds sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*> proofend; theorem Th17: :: BORSUK_7:17 for r1, r2, r3 being real number holds Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2) proofend; theorem Th18: :: BORSUK_7:18 for c being complex number for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2) proofend; theorem Th19: :: BORSUK_7:19 for c being complex number for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2) proofend; theorem Th20: :: BORSUK_7:20 for f being real-valued FinSequence st Sum f <> 0 holds Sum (f (/) (Sum f)) = 1 proofend; Lm6: 1,2,3 are_mutually_different proofend; definition let a, b, c, x, y, z be set ; func(a,b,c) --> (x,y,z) -> set equals :: BORSUK_7:def 1 ((a,b) --> (x,y)) +* (c .--> z); coherence ((a,b) --> (x,y)) +* (c .--> z) is set ; end; :: deftheorem defines --> BORSUK_7:def_1_:_ for a, b, c, x, y, z being set holds (a,b,c) --> (x,y,z) = ((a,b) --> (x,y)) +* (c .--> z); registration let a, b, c, x, y, z be set ; cluster(a,b,c) --> (x,y,z) -> Relation-like Function-like ; coherence ( (a,b,c) --> (x,y,z) is Function-like & (a,b,c) --> (x,y,z) is Relation-like ) ; end; theorem :: BORSUK_7:21 for a, b, x, y, z being set for c being complex number holds dom ((a,b,c) --> (x,y,z)) = {a,b,c} by BVFUNC14:11; theorem :: BORSUK_7:22 for a, b, x, y, z being set for c being complex number holds rng ((a,b,c) --> (x,y,z)) c= {x,y,z} proofend; theorem :: BORSUK_7:23 for a, x, y, z being set holds (a,a,a) --> (x,y,z) = a .--> z proofend; theorem :: BORSUK_7:24 for a, b, x, y, z being set holds (a,a,b) --> (x,y,z) = (a,b) --> (y,z) by FUNCT_4:81; theorem Th25: :: BORSUK_7:25 for a, b, x, y, z being set st a <> b holds (a,b,a) --> (x,y,z) = (a,b) --> (z,y) proofend; theorem Th26: :: BORSUK_7:26 for a, b, x, y, z being set holds (a,b,b) --> (x,y,z) = (a,b) --> (x,z) proofend; theorem :: BORSUK_7:27 for a, b, x, y, z being set for c being complex number st a <> b & a <> c holds ((a,b,c) --> (x,y,z)) . a = x by BVFUNC14:13; theorem Th28: :: BORSUK_7:28 for a, b, x, y, z being set for c being complex number st a,b,c are_mutually_different holds ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z ) proofend; theorem Th29: :: BORSUK_7:29 for a, b, x, y, z being set for c being complex number for f being Function st dom f = {a,b,c} & f . a = x & f . b = y & f . c = z holds f = (a,b,c) --> (x,y,z) proofend; theorem Th30: :: BORSUK_7:30 for a, b being set for c being complex number holds <*a,b,c*> = (1,2,3) --> (a,b,c) proofend; theorem Th31: :: BORSUK_7:31 for a, b, x, y, z being set for c being complex number st a,b,c are_mutually_different holds product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} proofend; theorem Th32: :: BORSUK_7:32 for a, b being set for c being complex number for A, B, C, D, E, F being set st A c= B & C c= D & E c= F holds product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) proofend; theorem Th33: :: BORSUK_7:33 for a, b, x, X, y, Y, z, Z being set for c being complex number st a,b,c are_mutually_different & x in X & y in Y & z in Z holds (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) proofend; definition let f be Function; attrf is odd means :Def2: :: BORSUK_7:def 2 for x, y being complex-valued Function st x in dom f & - x in dom f & y = f . x holds f . (- x) = - y; end; :: deftheorem Def2 defines odd BORSUK_7:def_2_:_ for f being Function holds ( f is odd iff for x, y being complex-valued Function st x in dom f & - x in dom f & y = f . x holds f . (- x) = - y ); registration cluster {} -> odd ; coherence {} is odd proofend; end; registration cluster Relation-like Function-like complex-functions-valued odd for set ; existence ex b1 being complex-functions-valued Function st b1 is odd proofend; end; set TC2 = Tunit_circle 2; set TC3 = Tunit_circle 3; Lm7: the carrier of (Tunit_circle 3) = Sphere (|[0,0,0]|,1) by EUCLID_5:4, TOPREALB:9; theorem :: BORSUK_7:34 for p being Point of (TOP-REAL 3) holds sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*> proofend; theorem Th35: :: BORSUK_7:35 for p being Point of (TOP-REAL 3) holds Sum (sqr p) = (((p `1) ^2) + ((p `2) ^2)) + ((p `3) ^2) proofend; reconsider QQ = RAT as Subset of REAL by NUMBERS:12; set RR = R^1 | (R^1 QQ); Lm8: the carrier of (R^1 | (R^1 QQ)) = QQ by PRE_TOPC:8; theorem Th36: :: BORSUK_7:36 for r being real number for S being Subset of R^1 st S = RAT holds RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) proofend; theorem Th37: :: BORSUK_7:37 for r being real number for S being Subset of R^1 st S = RAT holds RAT /\ ].r,+infty.[ is open Subset of (R^1 | S) proofend; Lm9: now__::_thesis:_for_T_being_non_empty_connected_TopSpace for_f_being_Function_of_T,(R^1_|_(R^1_QQ)) for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_f_&_f_._x_<_f_._y_holds_ ex_Q1,_Q2_being_Subset_of_(Image_f)_st_ (_Q1_misses_Q2_&_Q1_<>_{}_(Image_f)_&_Q2_<>_{}_(Image_f)_&_Q1_is_open_&_Q2_is_open_&_[#]_(Image_f)_=_Q1_\/_Q2_) let T be non empty connected TopSpace; ::_thesis: for f being Function of T,(R^1 | (R^1 QQ)) for x, y being set st x in dom f & y in dom f & f . x < f . y holds ex Q1, Q2 being Subset of (Image f) st ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) let f be Function of T,(R^1 | (R^1 QQ)); ::_thesis: for x, y being set st x in dom f & y in dom f & f . x < f . y holds ex Q1, Q2 being Subset of (Image f) st ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) let x, y be set ; ::_thesis: ( x in dom f & y in dom f & f . x < f . y implies ex Q1, Q2 being Subset of (Image f) st ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) ) assume A1: ( x in dom f & y in dom f ) ; ::_thesis: ( f . x < f . y implies ex Q1, Q2 being Subset of (Image f) st ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) ) assume f . x < f . y ; ::_thesis: ex Q1, Q2 being Subset of (Image f) st ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) then consider r being real irrational number such that A2: ( f . x < r & r < f . y ) by BORSUK_5:27; set GX = Image f; A3: ( f . x in rng f & f . y in rng f ) by A1, FUNCT_1:def_3; A4: [#] (Image f) = rng f by WAYBEL18:9; thus ex Q1, Q2 being Subset of (Image f) st ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) ::_thesis: verum proof set Q1 = { q where q is Element of RAT : ( q in rng f & q < r ) } ; set Q2 = { q where q is Element of RAT : ( q in rng f & q > r ) } ; { q where q is Element of RAT : ( q in rng f & q < r ) } c= rng f proof let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in { q where q is Element of RAT : ( q in rng f & q < r ) } or x in rng f ) assume x in { q where q is Element of RAT : ( q in rng f & q < r ) } ; ::_thesis: x in rng f then ex q being Element of RAT st ( x = q & q in rng f & q < r ) ; hence x in rng f ; ::_thesis: verum end; then reconsider Q1 = { q where q is Element of RAT : ( q in rng f & q < r ) } as Subset of (Image f) by WAYBEL18:9; { q where q is Element of RAT : ( q in rng f & q > r ) } c= rng f proof let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in { q where q is Element of RAT : ( q in rng f & q > r ) } or x in rng f ) assume x in { q where q is Element of RAT : ( q in rng f & q > r ) } ; ::_thesis: x in rng f then ex q being Element of RAT st ( x = q & q in rng f & q > r ) ; hence x in rng f ; ::_thesis: verum end; then reconsider Q2 = { q where q is Element of RAT : ( q in rng f & q > r ) } as Subset of (Image f) by WAYBEL18:9; take Q1 ; ::_thesis: ex Q2 being Subset of (Image f) st ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) take Q2 ; ::_thesis: ( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) thus Q1 misses Q2 ::_thesis: ( Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) proof assume not Q1 misses Q2 ; ::_thesis: contradiction then consider x being set such that A5: ( x in Q1 & x in Q2 ) by XBOOLE_0:3; ( ex q being Element of RAT st ( x = q & q in rng f & q > r ) & ex q being Element of RAT st ( x = q & q in rng f & q < r ) ) by A5; hence contradiction ; ::_thesis: verum end; ( f . x in Q1 & f . y in Q2 ) by A2, A3, Lm8; hence ( Q1 <> {} (Image f) & Q2 <> {} (Image f) ) ; ::_thesis: ( Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) reconsider G1 = RAT /\ ].-infty,r.[ as open Subset of (R^1 | (R^1 QQ)) by Th36; reconsider G2 = RAT /\ ].r,+infty.[ as open Subset of (R^1 | (R^1 QQ)) by Th37; Q1 = G1 /\ the carrier of (Image f) proof thus Q1 c= G1 /\ the carrier of (Image f) :: according toXBOOLE_0:def_10 ::_thesis: G1 /\ the carrier of (Image f) c= Q1 proof let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in Q1 or x in G1 /\ the carrier of (Image f) ) assume x in Q1 ; ::_thesis: x in G1 /\ the carrier of (Image f) then consider q being Element of RAT such that A6: x = q and A7: q in rng f and A8: q < r ; q in ].-infty,r.[ by A8, XXREAL_1:233; then q in G1 by XBOOLE_0:def_4; hence x in G1 /\ the carrier of (Image f) by A4, A6, A7, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in G1 /\ the carrier of (Image f) or x in Q1 ) assume A9: x in G1 /\ the carrier of (Image f) ; ::_thesis: x in Q1 then A10: x in the carrier of (Image f) by XBOOLE_0:def_4; A11: x in G1 by A9, XBOOLE_0:def_4; then reconsider x = x as Element of RAT by XBOOLE_0:def_4; x in ].-infty,r.[ by A11, XBOOLE_0:def_4; then x < r by XXREAL_1:233; hence x in Q1 by A4, A10; ::_thesis: verum end; hence Q1 is open by TSP_1:def_1; ::_thesis: ( Q2 is open & [#] (Image f) = Q1 \/ Q2 ) Q2 = G2 /\ the carrier of (Image f) proof thus Q2 c= G2 /\ the carrier of (Image f) :: according toXBOOLE_0:def_10 ::_thesis: G2 /\ the carrier of (Image f) c= Q2 proof let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in Q2 or x in G2 /\ the carrier of (Image f) ) assume x in Q2 ; ::_thesis: x in G2 /\ the carrier of (Image f) then consider q being Element of RAT such that A12: x = q and A13: q in rng f and A14: q > r ; q in ].r,+infty.[ by A14, XXREAL_1:235; then q in G2 by XBOOLE_0:def_4; hence x in G2 /\ the carrier of (Image f) by A4, A12, A13, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in G2 /\ the carrier of (Image f) or x in Q2 ) assume A15: x in G2 /\ the carrier of (Image f) ; ::_thesis: x in Q2 then A16: x in the carrier of (Image f) by XBOOLE_0:def_4; A17: x in G2 by A15, XBOOLE_0:def_4; then reconsider x = x as Element of RAT by XBOOLE_0:def_4; x in ].r,+infty.[ by A17, XBOOLE_0:def_4; then x > r by XXREAL_1:235; hence x in Q2 by A4, A16; ::_thesis: verum end; hence Q2 is open by TSP_1:def_1; ::_thesis: [#] (Image f) = Q1 \/ Q2 thus Q1 \/ Q2 = [#] (Image f) ::_thesis: verum proof thus Q1 \/ Q2 c= [#] (Image f) ; :: according toXBOOLE_0:def_10 ::_thesis: [#] (Image f) c= Q1 \/ Q2 let x be Element of (Image f); :: according toLATTICE7:def_1 ::_thesis: ( not x in [#] (Image f) or x in Q1 \/ Q2 ) assume A18: x in [#] (Image f) ; ::_thesis: x in Q1 \/ Q2 ( x < r or x > r ) by Lm8, A4, XXREAL_0:1; then ( x in Q1 or x in Q2 ) by A18, Lm8, A4; hence x in Q1 \/ Q2 by XBOOLE_0:def_3; ::_thesis: verum end; end; end; registration let X be non empty connected TopSpace; let Y be non empty TopSpace; let f be continuous Function of X,Y; cluster Image f -> connected ; coherence Image f is connected proofend; end; theorem Th38: :: BORSUK_7:38 for S being Subset of R^1 st S = RAT holds for T being connected TopSpace for f being Function of T,(R^1 | S) st f is continuous holds f is constant proofend; theorem Th39: :: BORSUK_7:39 for a, b being real number for f being continuous Function of (Closed-Interval-TSpace (a,b)),R^1 for g being PartFunc of REAL,REAL st a <= b & f = g holds g is continuous proofend; definition let s be Point of R^1; let r be real number ; :: original:+ redefine funcs + r -> Point of R^1; coherence s + r is Point of R^1 by TOPMETR:17, XREAL_0:def_1; end; definition let s be Point of R^1; let r be real number ; :: original:- redefine funcs - r -> Point of R^1; coherence s - r is Point of R^1 by TOPMETR:17, XREAL_0:def_1; end; definition let X be set ; let f be Function of X,R^1; let r be real number ; :: original:+ redefine funcf + r -> Function of X,R^1; coherence r + f is Function of X,R^1 proofend; end; definition let X be set ; let f be Function of X,R^1; let r be real number ; :: original:- redefine funcf - r -> Function of X,R^1; coherence f - r is Function of X,R^1 proofend; end; definition let s, t be Point of R^1; let f be Path of s,t; let r be real number ; :: original:+ redefine funcf + r -> Path of s + r,t + r; coherence r + f is Path of s + r,t + r proofend; :: original:- redefine funcf - r -> Path of s - r,t - r; coherence f - r is Path of s - r,t - r proofend; end; definition func c[100] -> Point of (Tunit_circle 3) equals :: BORSUK_7:def 3 |[1,0,0]|; coherence |[1,0,0]| is Point of (Tunit_circle 3) proofend; end; :: deftheorem defines c[100] BORSUK_7:def_3_:_ c[100] = |[1,0,0]|; reconsider c100 = c[100] as Point of (TOP-REAL 3) ; reconsider c100a = c[100] as Point of (Tunit_circle (2 + 1)) ; definition func c[-100] -> Point of (Tunit_circle 3) equals :: BORSUK_7:def 4 |[(- 1),0,0]|; coherence |[(- 1),0,0]| is Point of (Tunit_circle 3) proofend; end; :: deftheorem defines c[-100] BORSUK_7:def_4_:_ c[-100] = |[(- 1),0,0]|; reconsider mc100 = c[-100] as Point of (TOP-REAL 3) ; theorem Th40: :: BORSUK_7:40 - c[100] = c[-100] proofend; theorem :: BORSUK_7:41 - c[-100] = c[100] by Th40; theorem :: BORSUK_7:42 c[100] - c[-100] = |[2,0,0]| proofend; theorem :: BORSUK_7:43 for p being Point of (TOP-REAL 2) holds ( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) ) proofend; theorem :: BORSUK_7:44 for p being Point of (TOP-REAL 2) holds p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * )) proofend; theorem Th45: :: BORSUK_7:45 for i being Integer for p1, p2 being Point of (TOP-REAL 2) st |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) holds p1 = p2 proofend; set CM = CircleMap ; theorem Th46: :: BORSUK_7:46 for r being real number for p being Point of (TOP-REAL 2) st p = CircleMap . r holds Arg p = (2 * PI) * (frac r) proofend; theorem Th47: :: BORSUK_7:47 for p1, p2 being Point of (TOP-REAL 3) for u1, u2 being Point of (Euclid 3) st u1 = p1 & u2 = p2 holds (Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2)) proofend; theorem Th48: :: BORSUK_7:48 for r being real number for p being Point of (TOP-REAL 3) for e being Point of (Euclid 3) st p = e & p `3 = 0 holds product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r) proofend; theorem Th49: :: BORSUK_7:49 for i being Integer for c being complex number for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) proofend; theorem :: BORSUK_7:50 for i being Integer for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i)) proofend; theorem Th51: :: BORSUK_7:51 for s being Real for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.| proofend; theorem Th52: :: BORSUK_7:52 for s being Real for p being Point of (TOP-REAL 2) holds Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s)) proofend; theorem Th53: :: BORSUK_7:53 for s being Real for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i) proofend; theorem Th54: :: BORSUK_7:54 for s being Real holds (Rotate s) . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2) proofend; theorem Th55: :: BORSUK_7:55 for s being Real for p being Point of (TOP-REAL 2) st (Rotate s) . p = 0. (TOP-REAL 2) holds p = 0. (TOP-REAL 2) proofend; theorem Th56: :: BORSUK_7:56 for s being Real for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p proofend; theorem :: BORSUK_7:57 for s being Real holds (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2) proofend; theorem Th58: :: BORSUK_7:58 for r being real number for s being Real for p being Point of (TOP-REAL 2) holds ( p in Sphere ((0. (TOP-REAL 2)),r) iff (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) ) proofend; theorem Th59: :: BORSUK_7:59 for r being real non negative number for s being Real holds (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) proofend; definition let r be real non negative number ; let s be Real; func RotateCircle (r,s) -> Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r)) equals :: BORSUK_7:def 5 (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)); coherence (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)) is Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r)) proofend; end; :: deftheorem defines RotateCircle BORSUK_7:def_5_:_ for r being real non negative number for s being Real holds RotateCircle (r,s) = (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)); registration let r be real non negative number ; let s be Real; cluster RotateCircle (r,s) -> being_homeomorphism ; coherence RotateCircle (r,s) is being_homeomorphism proofend; end; theorem Th60: :: BORSUK_7:60 for r2, r1 being real number for p being Point of (TOP-REAL 2) st p = CircleMap . r2 holds (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2) proofend; begin definition let n be non empty Nat; let p be Point of (TOP-REAL n); let r be real non negative number ; func CircleIso (p,r) -> Function of (Tunit_circle n),(Tcircle (p,r)) means :Def6: :: BORSUK_7:def 6 for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds it . a = (r * b) + p; existence ex b1 being Function of (Tunit_circle n),(Tcircle (p,r)) st for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds b1 . a = (r * b) + p proofend; uniqueness for b1, b2 being Function of (Tunit_circle n),(Tcircle (p,r)) st ( for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds b1 . a = (r * b) + p ) & ( for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds b2 . a = (r * b) + p ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines CircleIso BORSUK_7:def_6_:_ for n being non empty Nat for p being Point of (TOP-REAL n) for r being real non negative number for b4 being Function of (Tunit_circle n),(Tcircle (p,r)) holds ( b4 = CircleIso (p,r) iff for a being Point of (Tunit_circle n) for b being Point of (TOP-REAL n) st a = b holds b4 . a = (r * b) + p ); registration let n be non empty Nat; let p be Point of (TOP-REAL n); let r be real positive number ; cluster CircleIso (p,r) -> being_homeomorphism ; coherence CircleIso (p,r) is being_homeomorphism proofend; end; definition func SphereMap -> Function of R^1,(Tunit_circle 3) means :Def7: :: BORSUK_7:def 7 for x being real number holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|; existence ex b1 being Function of R^1,(Tunit_circle 3) st for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| proofend; uniqueness for b1, b2 being Function of R^1,(Tunit_circle 3) st ( for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) & ( for x being real number holds b2 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines SphereMap BORSUK_7:def_7_:_ for b1 being Function of R^1,(Tunit_circle 3) holds ( b1 = SphereMap iff for x being real number holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ); set SM = SphereMap ; theorem :: BORSUK_7:61 for i being Integer holds SphereMap . i = c[100] proofend; Lm10: sin is Function of R^1,R^1 proofend; Lm11: cos is Function of R^1,R^1 proofend; Lm12: for r being real number holds SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| proofend; registration cluster SphereMap -> continuous ; coherence SphereMap is continuous proofend; end; definition let r be real number ; func eLoop r -> Function of I[01],(Tunit_circle 3) means :Def8: :: BORSUK_7:def 8 for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|; existence ex b1 being Function of I[01],(Tunit_circle 3) st for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| proofend; uniqueness for b1, b2 being Function of I[01],(Tunit_circle 3) st ( for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) & ( for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines eLoop BORSUK_7:def_8_:_ for r being real number for b2 being Function of I[01],(Tunit_circle 3) holds ( b2 = eLoop r iff for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ); theorem Th62: :: BORSUK_7:62 for r being real number holds eLoop r = SphereMap * (ExtendInt r) proofend; definition let i be Integer; :: original:eLoop redefine func eLoop i -> Loop of c[100] ; coherence eLoop i is Loop of c[100] proofend; end; registration let i be Integer; cluster eLoop i -> nullhomotopic for Loop of c[100] ; coherence for b1 being Loop of c[100] st b1 = eLoop i holds b1 is nullhomotopic proofend; end; theorem Th63: :: BORSUK_7:63 for n being Nat for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds |.(p (/) |.p.|).| = 1 proofend; definition let n be Nat; let p be Point of (TOP-REAL n); assume A1: p <> 0. (TOP-REAL n) ; func Rn->S1 p -> Point of (Tcircle ((0. (TOP-REAL n)),1)) equals :Def9: :: BORSUK_7:def 9 p (/) |.p.|; coherence p (/) |.p.| is Point of (Tcircle ((0. (TOP-REAL n)),1)) proofend; end; :: deftheorem Def9 defines Rn->S1 BORSUK_7:def_9_:_ for n being Nat for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds Rn->S1 p = p (/) |.p.|; definition let n be non zero Nat; let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); set TC4 = Tcircle ((0. (TOP-REAL (n + 1))),1); set TC3 = Tunit_circle (n + 1); set TC2 = Tunit_circle n; func Sn1->Sn f -> Function of (Tunit_circle (n + 1)),(Tunit_circle n) means :Def10: :: BORSUK_7:def 10 for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds it . x = Rn->S1 ((f . x) - (f . y)); existence ex b1 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) st for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b1 . x = Rn->S1 ((f . x) - (f . y)) proofend; uniqueness for b1, b2 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) st ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b1 . x = Rn->S1 ((f . x) - (f . y)) ) & ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b2 . x = Rn->S1 ((f . x) - (f . y)) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines Sn1->Sn BORSUK_7:def_10_:_ for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) for b3 being Function of (Tunit_circle (n + 1)),(Tunit_circle n) holds ( b3 = Sn1->Sn f iff for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds b3 . x = Rn->S1 ((f . x) - (f . y)) ); definition let x0, y0 be Point of (Tunit_circle 2); let xt be set ; let f be Path of x0,y0; assume A1: xt in CircleMap " {x0} ; func liftPath (f,xt) -> Function of I[01],R^1 means :Def11: :: BORSUK_7:def 11 ( it . 0 = xt & f = CircleMap * it & it is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds it = f1 ) ); existence ex b1 being Function of I[01],R^1 st ( b1 . 0 = xt & f = CircleMap * b1 & b1 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds b1 = f1 ) ) by A1, TOPALG_5:23; uniqueness for b1, b2 being Function of I[01],R^1 st b1 . 0 = xt & f = CircleMap * b1 & b1 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds b1 = f1 ) & b2 . 0 = xt & f = CircleMap * b2 & b2 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds b2 = f1 ) holds b1 = b2 ; end; :: deftheorem Def11 defines liftPath BORSUK_7:def_11_:_ for x0, y0 being Point of (Tunit_circle 2) for xt being set for f being Path of x0,y0 st xt in CircleMap " {x0} holds for b5 being Function of I[01],R^1 holds ( b5 = liftPath (f,xt) iff ( b5 . 0 = xt & f = CircleMap * b5 & b5 is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds b5 = f1 ) ) ); definition let n be Nat; let p, x, y be Point of (TOP-REAL n); let r be real number ; predx,y are_antipodals_of p,r means :Def12: :: BORSUK_7:def 12 ( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) ); end; :: deftheorem Def12 defines are_antipodals_of BORSUK_7:def_12_:_ for n being Nat for p, x, y being Point of (TOP-REAL n) for r being real number holds ( x,y are_antipodals_of p,r iff ( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) ) ); definition let n be Nat; let p, x, y be Point of (TOP-REAL n); let r be real number ; let f be Function; predx,y are_antipodals_of p,r,f means :Def13: :: BORSUK_7:def 13 ( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y ); end; :: deftheorem Def13 defines are_antipodals_of BORSUK_7:def_13_:_ for n being Nat for p, x, y being Point of (TOP-REAL n) for r being real number for f being Function holds ( x,y are_antipodals_of p,r,f iff ( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y ) ); definition let m, n be Nat; let p be Point of (TOP-REAL m); let r be real number ; let f be Function of (Tcircle (p,r)),(TOP-REAL n); attrf is with_antipodals means :Def14: :: BORSUK_7:def 14 ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f; end; :: deftheorem Def14 defines with_antipodals BORSUK_7:def_14_:_ for m, n being Nat for p being Point of (TOP-REAL m) for r being real number for f being Function of (Tcircle (p,r)),(TOP-REAL n) holds ( f is with_antipodals iff ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f ); notation let m, n be Nat; let p be Point of (TOP-REAL m); let r be real number ; let f be Function of (Tcircle (p,r)),(TOP-REAL n); antonym without_antipodals f for with_antipodals ; end; theorem Th64: :: BORSUK_7:64 for n being non empty Nat for r being real non negative number for x being Point of (TOP-REAL n) st x is Point of (Tcircle ((0. (TOP-REAL n)),r)) holds x, - x are_antipodals_of 0. (TOP-REAL n),r proofend; theorem Th65: :: BORSUK_7:65 for n being non empty Nat for p, x, y, x1, y1 being Point of (TOP-REAL n) for r being real positive number st x,y are_antipodals_of 0. (TOP-REAL n),1 & x1 = (CircleIso (p,r)) . x & y1 = (CircleIso (p,r)) . y holds x1,y1 are_antipodals_of p,r proofend; theorem Th66: :: BORSUK_7:66 for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) for x being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st f is without_antipodals holds (f . x) - (f . (- x)) <> 0. (TOP-REAL n) proofend; theorem Th67: :: BORSUK_7:67 for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st f is without_antipodals holds Sn1->Sn f is odd proofend; theorem Th68: :: BORSUK_7:68 for n being non zero Nat for f, g, B1 being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st g = f (-) & B1 = f <--> g & f is without_antipodals holds Sn1->Sn f = B1 ((n NormF) * B1) proofend; Lm13: for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st f is without_antipodals & f is continuous holds Sn1->Sn f is continuous proofend; deffunc H1( Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2)) -> Element of bool [: the carrier of I[01], the carrier of (Tunit_circle 2):] = (Sn1->Sn $1) * (eLoop 1); Lm14: for s being real number for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & 0 <= s & s <= 1 / 2 holds H1(f) . (s + (1 / 2)) = - (H1(f) . s) proofend; defpred S1[ Point of R^1, Point of R^1, Integer] means $1 = $2 + ($3 / 2); Lm15: now__::_thesis:_for_a,_b_being_Point_of_R^1_st_CircleMap_._a_=_-_(CircleMap_._b)_holds_ ex_I_being_odd_Integer_st_S1[a,b,I] let a, b be Point of R^1; ::_thesis: ( CircleMap . a = - (CircleMap . b) implies ex I being odd Integer st S1[a,b,I] ) assume A1: CircleMap . a = - (CircleMap . b) ; ::_thesis: ex I being odd Integer st S1[a,b,I] thus ex I being odd Integer st S1[a,b,I] ::_thesis: verum proof A2: ( CircleMap . a = |[(cos ((2 * PI) * a)),(sin ((2 * PI) * a))]| & CircleMap . b = |[(cos ((2 * PI) * b)),(sin ((2 * PI) * b))]| ) by TOPREALB:def_11; A3: - |[(cos ((2 * PI) * b)),(sin ((2 * PI) * b))]| = |[(- (cos ((2 * PI) * b))),(- (sin ((2 * PI) * b)))]| by EUCLID:60; then A4: cos ((2 * PI) * a) = - (cos ((2 * PI) * b)) by A1, A2, FINSEQ_1:77 .= cos (PI + ((2 * PI) * b)) by SIN_COS:79 ; sin ((2 * PI) * a) = - (sin ((2 * PI) * b)) by A1, A2, A3, FINSEQ_1:77 .= sin (PI + ((2 * PI) * b)) by SIN_COS:79 ; then consider i being Integer such that A5: (2 * PI) * a = (PI + ((2 * PI) * b)) + ((2 * PI) * i) by A4, Th11; A6: 2 * a = (PI * (2 * a)) / PI by XCMPLX_1:89 .= (PI * ((1 + (2 * b)) + (2 * i))) / PI by A5 .= (1 + (2 * b)) + (2 * i) by XCMPLX_1:89 ; take I = (2 * i) + 1; ::_thesis: S1[a,b,I] thus S1[a,b,I] by A6; ::_thesis: verum end; end; Lm16: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & f is continuous holds H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a proofend; Lm17: now__::_thesis:_for_f_being_Function_of_(Tcircle_((0._(TOP-REAL_(2_+_1))),1)),(TOP-REAL_2) for_s_being_real_number_ for_xt_being_set_st_f_is_without_antipodals_&_f_is_continuous_&_xt_in_CircleMap_"_{((Sn1->Sn_f)_._c[100])}_&_0_<=_s_&_s_<=_1_/_2_holds_ ex_IT_being_odd_Integer_st_ for_L_being_Loop_of_(Sn1->Sn_f)_._c100a_st_L_=_H1(f)_holds_ (liftPath_(L,xt))_._(s_+_(1_/_2))_=_((liftPath_(L,xt))_._s)_+_(IT_/_2) let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: for s being real number for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 holds ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) let s be real number ; ::_thesis: for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 holds ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) let xt be set ; ::_thesis: ( f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} & 0 <= s & s <= 1 / 2 implies ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) ) assume that A1: ( f is without_antipodals & f is continuous ) and A2: xt in CircleMap " {((Sn1->Sn f) . c[100])} and A3: ( 0 <= s & s <= 1 / 2 ) ; ::_thesis: ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) thus ex IT being odd Integer st for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) ::_thesis: verum proof reconsider s = s as Point of I[01] by A3, Lm3; reconsider L = H1(f) as Loop of (Sn1->Sn f) . c100a by A1, Lm16; set l = liftPath (L,xt); set t = R^1 (s + (1 / 2)); reconsider t1 = R^1 (s + (1 / 2)) as Point of I[01] by A3, Lm4; A4: H1(f) = CircleMap * (liftPath (L,xt)) by A2, Def11; ( (CircleMap * (liftPath (L,xt))) . t1 = CircleMap . ((liftPath (L,xt)) . t1) & (CircleMap * (liftPath (L,xt))) . s = CircleMap . ((liftPath (L,xt)) . s) ) by FUNCT_2:15; then CircleMap . ((liftPath (L,xt)) . (R^1 (s + (1 / 2)))) = - (CircleMap . ((liftPath (L,xt)) . s)) by A4, A3, A1, Lm14; then consider I being odd Integer such that A5: S1[(liftPath (L,xt)) . t1,(liftPath (L,xt)) . s,I] by Lm15; take I ; ::_thesis: for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) thus for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) by A5; ::_thesis: verum end; end; defpred S2[ Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2), set , Integer] means for L being Loop of (Sn1->Sn $1) . c100a st L = H1($1) holds for s being real number st 0 <= s & s <= 1 / 2 holds (liftPath (L,$2)) . (s + (1 / 2)) = ((liftPath (L,$2)) . s) + ($3 / 2); Lm18: now__::_thesis:_for_f_being_Function_of_(Tcircle_((0._(TOP-REAL_(2_+_1))),1)),(TOP-REAL_2) for_xt_being_set_st_f_is_without_antipodals_&_f_is_continuous_&_xt_in_CircleMap_"_{((Sn1->Sn_f)_._c[100])}_holds_ ex_I_being_odd_Integer_st_S2[f,xt,I] let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} holds ex I being odd Integer st S2[f,xt,I] let xt be set ; ::_thesis: ( f is without_antipodals & f is continuous & xt in CircleMap " {((Sn1->Sn f) . c[100])} implies ex I being odd Integer st S2[f,xt,I] ) assume that A1: ( f is without_antipodals & f is continuous ) and A2: xt in CircleMap " {((Sn1->Sn f) . c[100])} ; ::_thesis: ex I being odd Integer st S2[f,xt,I] reconsider L1 = H1(f) as Loop of (Sn1->Sn f) . c100a by A1, Lm16; thus ex I being odd Integer st S2[f,xt,I] ::_thesis: verum proof set l1 = liftPath (L1,xt); set S = [.0,(1 / 2).]; set AF = AffineMap (1,(1 / 2)); set W = 2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))); dom (AffineMap (1,(1 / 2))) = REAL by FUNCT_2:def_1; then A3: dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) = [.0,(1 / 2).] by RELAT_1:62; A4: dom (liftPath (L1,xt)) = the carrier of I[01] by FUNCT_2:def_1; A5: rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) c= the carrier of I[01] proof let y be set ; :: according toTARSKI:def_3 ::_thesis: ( not y in rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) or y in the carrier of I[01] ) assume y in rng ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) ; ::_thesis: y in the carrier of I[01] then consider x being set such that A6: x in dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) and A7: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . x = y by FUNCT_1:def_3; reconsider x = x as real number by A6; A8: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . x = (AffineMap (1,(1 / 2))) . x by A6, FUNCT_1:47 .= (1 * x) + (1 / 2) by FCONT_1:def_4 ; ( 0 <= x & x <= 1 / 2 ) by A6, A3, XXREAL_1:1; then ( Q + (1 / 2) <= x + (1 / 2) & x + (1 / 2) <= (1 / 2) + (1 / 2) ) by XREAL_1:6; hence y in the carrier of I[01] by A7, A8, BORSUK_1:43; ::_thesis: verum end; A9: dom (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) = (dom ((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]))) /\ (dom (liftPath (L1,xt))) by VALUED_1:12 .= (dom ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) /\ (dom (liftPath (L1,xt))) by A4, A5, RELAT_1:27 .= [.0,(1 / 2).] by A3, A4, BORSUK_1:40, XBOOLE_1:28, XXREAL_1:34 ; A10: dom (2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt)))) = dom (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) by VALUED_1:def_5; rng (2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt)))) c= REAL by VALUED_0:def_3; then reconsider W = 2 (#) (((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) as PartFunc of REAL,REAL by A9, A10, RELSET_1:4; consider ITj0 being odd Integer such that A11: for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (j0 + (1 / 2)) = ((liftPath (L,xt)) . j0) + (ITj0 / 2) by A1, A2, Lm17; take ITj0 ; ::_thesis: S2[f,xt,ITj0] let L be Loop of (Sn1->Sn f) . c100a; ::_thesis: ( L = H1(f) implies for s being real number st 0 <= s & s <= 1 / 2 holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) ) assume A12: L = H1(f) ; ::_thesis: for s being real number st 0 <= s & s <= 1 / 2 holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) let s be real number ; ::_thesis: ( 0 <= s & s <= 1 / 2 implies (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) ) assume A13: ( 0 <= s & s <= 1 / 2 ) ; ::_thesis: (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) set l = liftPath (L,xt); A14: s in [.0,(1 / 2).] by A13, XXREAL_1:1; A15: 0 in [.0,(1 / 2).] by XXREAL_1:1; then A16: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . 0 = (AffineMap (1,(1 / 2))) . 0 by FUNCT_1:49 .= (1 * Q) + (1 / 2) by FCONT_1:def_4 ; A17: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . s = (AffineMap (1,(1 / 2))) . s by A14, FUNCT_1:49 .= (1 * s) + (1 / 2) by FCONT_1:def_4 ; consider ITs being odd Integer such that A18: for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITs / 2) by A1, A2, A13, Lm17; A19: (liftPath (L1,xt)) . (j0 + (1 / 2)) = ((liftPath (L1,xt)) . j0) + (ITj0 / 2) by A11; A20: (liftPath (L1,xt)) . (s + (1 / 2)) = ((liftPath (L1,xt)) . s) + (ITs / 2) by A18; A21: W . 0 = 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) . 0) by VALUED_1:6 .= 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) . 0) - ((liftPath (L1,xt)) . 0)) by A9, A15, VALUED_1:13 .= 2 * (((liftPath (L1,xt)) . (1 / 2)) - ((liftPath (L1,xt)) . 0)) by A16, A3, A15, FUNCT_1:13 .= 2 * (ITj0 / 2) by A19 ; A22: W . s = 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) . s) by VALUED_1:6 .= 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) . s) - ((liftPath (L1,xt)) . s)) by A9, A14, VALUED_1:13 .= 2 * (((liftPath (L1,xt)) . (s + (1 / 2))) - ((liftPath (L1,xt)) . s)) by A17, A3, A14, FUNCT_1:13 .= 2 * (ITs / 2) by A20 ; A23: rng W c= INT proof let y be set ; :: according toTARSKI:def_3 ::_thesis: ( not y in rng W or y in INT ) assume y in rng W ; ::_thesis: y in INT then consider s being set such that A24: s in dom W and A25: W . s = y by FUNCT_1:def_3; reconsider s = s as real number by A24; A26: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . s = (AffineMap (1,(1 / 2))) . s by A9, A10, A24, FUNCT_1:49 .= (1 * s) + (1 / 2) by FCONT_1:def_4 ; ( 0 <= s & s <= 1 / 2 ) by A9, A10, A24, XXREAL_1:1; then consider ITs being odd Integer such that A27: for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITs / 2) by A1, A2, Lm17; A28: (liftPath (L1,xt)) . (s + (1 / 2)) = ((liftPath (L1,xt)) . s) + (ITs / 2) by A27; W . s = 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - (liftPath (L1,xt))) . s) by VALUED_1:6 .= 2 * ((((liftPath (L1,xt)) * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) . s) - ((liftPath (L1,xt)) . s)) by A10, A24, VALUED_1:13 .= 2 * (((liftPath (L1,xt)) . (s + (1 / 2))) - ((liftPath (L1,xt)) . s)) by A26, A3, A9, A10, A24, FUNCT_1:13 .= 2 * (ITs / 2) by A28 ; hence y in INT by A25, INT_1:def_2; ::_thesis: verum end; set T = Closed-Interval-TSpace (0,(1 / 2)); A29: the carrier of (Closed-Interval-TSpace (0,(1 / 2))) = [.0,(1 / 2).] by TOPMETR:18; A30: rng W c= RAT by A23, NUMBERS:14, XBOOLE_1:1; reconsider SR = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17; reconsider W1 = W as Function of (Closed-Interval-TSpace (0,(1 / 2))),(R^1 | SR) by A10, A9, Lm8, A29, A23, FUNCT_2:2, NUMBERS:14, XBOOLE_1:1; A31: Closed-Interval-TSpace (0,(1 / 2)) is connected by TREAL_1:20; A32: R^1 | (R^1 (dom W)) = Closed-Interval-TSpace (0,(1 / 2)) by A10, A9, A29, PRE_TOPC:8, TSEP_1:5; reconsider f1 = R^1 ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) as Function of (Closed-Interval-TSpace (0,(1 / 2))),I[01] by A5, A3, A29, FUNCT_2:2; rng (liftPath (L1,xt)) c= REAL by TOPMETR:17; then reconsider ll1 = liftPath (L1,xt) as PartFunc of REAL,REAL by A4, BORSUK_1:40, RELSET_1:4; liftPath (L1,xt) is continuous by A2, Def11; then A33: ll1 is continuous by Th39, TOPMETR:20; (ll1 * ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).])) - ll1 is continuous by A33; then reconsider W = W as continuous PartFunc of REAL,REAL ; the carrier of (R^1 | (R^1 (rng W))) = rng W by PRE_TOPC:8; then A34: R^1 | (R^1 (rng W)) is SubSpace of R^1 | (R^1 QQ) by A30, Lm8, TSEP_1:4; R^1 W is continuous ; then W1 is continuous by A32, A34, PRE_TOPC:26; then W1 is constant by A31, Th38; hence (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) by A20, A12, A21, A22, A9, A10, A15, A14, FUNCT_1:def_10; ::_thesis: verum end; end; Lm19: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) for xt being Point of R^1 for L being Loop of (Sn1->Sn f) . c100a st L = H1(f) holds for I being Integer st S2[f,xt,I] holds (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I proofend; Lm20: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) st f is without_antipodals & f is continuous holds not H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a proofend; Lm21: for f being continuous Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) holds f is with_antipodals proofend; registration let n be non zero Nat; let r be real negative number ; let p be Point of (TOP-REAL (n + 1)); cluster Function-like quasi_total -> without_antipodals for Element of bool [: the carrier of (Tcircle (p,r)), the carrier of (TOP-REAL n):]; coherence for b1 being Function of (Tcircle (p,r)),(TOP-REAL n) holds b1 is without_antipodals proofend; end; :: [WP: ] Borsuk-Ulam_Theorem registration let r be real non negative number ; let p be Point of (TOP-REAL 3); cluster Function-like quasi_total continuous -> with_antipodals for Element of bool [: the carrier of (Tcircle (p,r)), the carrier of (TOP-REAL 2):]; coherence for b1 being Function of (Tcircle (p,r)),(TOP-REAL 2) st b1 is continuous holds b1 is with_antipodals proofend; end;