:: The {B}orsuk-Ulam Theorem
:: by Artur Korni{\l}owicz and Marco Riccardi
::
:: Copyright (c) 2011-2021 Association of Mizar Users

reconsider Q = 0 as Nat ;

set T2 = TOP-REAL 2;

set o2 = ;

set o = |[0,0,0]|;

set I = the carrier of I[01];

set II = the carrier of ;

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 ;

Lm1: the carrier of = [: the carrier of I[01], the carrier of I[01]:]
by BORSUK_1:def 2;

Lm2:
by TARSKI:def 1;

Lm3: now :: thesis: for s being Real st s <= 1 / 2 & 0 <= s holds
s in the carrier of I[01]
let s be Real; :: 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 st 0 <= s & s <= 1 / 2 holds
s + (1 / 2) in the carrier of I[01]
let s be Real; :: 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 st 0 <= r & 0 <= s & r ^2 = s ^2 holds
r = s
proof end;

theorem Th2: :: BORSUK_7:2
for r, s being Real st frac r >= frac s holds
frac (r - s) = (frac r) - (frac s)
proof end;

theorem Th3: :: BORSUK_7:3
for r, s being Real st frac r < frac s holds
frac (r - s) = ((frac r) - (frac s)) + 1
proof end;

theorem Th4: :: BORSUK_7:4
for r, s being Real ex i being Integer st
( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) )
proof end;

theorem Th5: :: BORSUK_7:5
for r being Real holds
( not sin r = 0 or r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) )
proof end;

theorem Th6: :: BORSUK_7:6
for r being Real holds
( not cos r = 0 or r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) )
proof end;

theorem Th7: :: BORSUK_7:7
for r being Real st sin r = 0 holds
ex i being Integer st r = PI * i
proof end;

theorem Th8: :: BORSUK_7:8
for r being Real st cos r = 0 holds
ex i being Integer st r = (PI / 2) + (PI * i)
proof end;

Lm5: now :: thesis: for r, s being Real st sin ((r - s) / 2) = 0 holds
ex i being Integer st r = s + ((2 * PI) * i)
let r, s be Real; :: 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 st sin r = sin s holds
ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) )
proof end;

theorem Th10: :: BORSUK_7:10
for r, s being Real st cos r = cos s holds
ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )
proof end;

theorem Th11: :: BORSUK_7:11
for r, s being Real st sin r = sin s & cos r = cos s holds
ex i being Integer st r = s + ((2 * PI) * i)
proof end;

theorem Th12: :: BORSUK_7:12
for i being Integer
for c1, c2 being Complex st |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) holds
c1 = c2
proof end;

registration
let f be one-to-one complex-valued Function;
let c be Complex;
cluster c + f -> one-to-one ;
coherence
f + c is one-to-one
proof end;
end;

registration
let f be one-to-one complex-valued Function;
let c be Complex;
cluster f - c -> one-to-one ;
coherence
f - c is one-to-one
;
end;

theorem :: BORSUK_7:13
canceled;

::$CT theorem Th13: :: BORSUK_7:14 for n being Nat holds - (0* n) = 0* n proof end; theorem Th14: :: BORSUK_7:15 for n being Nat for f being complex-valued Function st f <> 0* n holds - f <> 0* n proof end; theorem Th15: :: BORSUK_7:16 for r1, r2, r3 being Real holds sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*> proof end; theorem Th16: :: BORSUK_7:17 for r1, r2, r3 being Real holds Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2) proof end; theorem Th17: :: BORSUK_7:18 for c being Complex for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2) proof end; theorem Th18: :: BORSUK_7:19 for c being Complex for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2) proof end; theorem Th19: :: BORSUK_7:20 for f being real-valued FinSequence st Sum f <> 0 holds Sum (f (/) (Sum f)) = 1 proof end; Lm6: ; canceled; theorem :: BORSUK_7:21 canceled; theorem :: BORSUK_7:22 canceled; theorem :: BORSUK_7:23 canceled; theorem :: BORSUK_7:24 canceled; theorem :: BORSUK_7:25 canceled; theorem :: BORSUK_7:26 canceled; theorem :: BORSUK_7:27 canceled; theorem :: BORSUK_7:28 canceled; theorem :: BORSUK_7:29 canceled; ::$CD
::$CT 9 theorem Th20: :: BORSUK_7:30 for a, b, c being object holds <*a,b,c*> = (1,2,3) --> (a,b,c) proof end; theorem Th21: :: BORSUK_7:31 for a, b, c, x, y, z being object st a,b,c are_mutually_distinct holds product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} proof end; theorem Th22: :: BORSUK_7:32 for a, b, c being object 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)) proof end; theorem Th23: :: BORSUK_7:33 for a, b, c, x, y, z being object for X, Y, Z being set st a,b,c are_mutually_distinct & x in X & y in Y & z in Z holds (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) proof end; definition let f be Function; attr f is odd means :: BORSUK_7:def 1 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 defines odd BORSUK_7:def 1 : 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 ; end; registration existence ex b1 being complex-functions-valued Function st b1 is odd proof end; end; set TC2 = Tunit_circle 2; set TC3 = Tunit_circle 3; Lm7: the carrier of () = Sphere (|[0,0,0]|,1) by ; theorem :: BORSUK_7:34 for p being Point of () holds sqr p = <*((p 1) ^2),((p 2) ^2),((p 3) ^2)*> proof end; theorem Th25: :: BORSUK_7:35 for p being Point of () holds Sum (sqr p) = (((p 1) ^2) + ((p 2) ^2)) + ((p 3) ^2) proof end; 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 Th26: :: BORSUK_7:36 for r being Real for S being Subset of R^1 st S = RAT holds RAT /\ is open Subset of (R^1 | S) proof end; theorem Th27: :: BORSUK_7:37 for r being Real for S being Subset of R^1 st S = RAT holds RAT /\ is open Subset of (R^1 | S) proof end; 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 () st ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = 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 () st ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = 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 () st ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = 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 () st ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = Q1 \/ Q2 ) ) assume A1: ( x in dom f & y in dom f ) ; :: thesis: ( f . x < f . y implies ex Q1, Q2 being Subset of () st ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = Q1 \/ Q2 ) ) assume f . x < f . y ; :: thesis: ex Q1, Q2 being Subset of () st ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = Q1 \/ Q2 ) then consider r being irrational Real 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 ; A4: [#] () = rng f by WAYBEL18:9; thus ex Q1, Q2 being Subset of () st ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = 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 object ; :: according to TARSKI: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 () by WAYBEL18:9; { q where q is Element of RAT : ( q in rng f & q > r ) } c= rng f proof let x be object ; :: according to TARSKI: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 () by WAYBEL18:9; take Q1 ; :: thesis: ex Q2 being Subset of () st ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = Q1 \/ Q2 ) take Q2 ; :: thesis: ( Q1 misses Q2 & Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = Q1 \/ Q2 ) thus Q1 misses Q2 :: thesis: ( Q1 <> {} () & Q2 <> {} () & Q1 is open & Q2 is open & [#] () = Q1 \/ Q2 ) proof assume not Q1 misses Q2 ; :: thesis: contradiction then consider x being object 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 <> {} () & Q2 <> {} () ) ; :: thesis: ( Q1 is open & Q2 is open & [#] () = Q1 \/ Q2 ) reconsider G1 = RAT /\ as open Subset of (R^1 | (R^1 QQ)) by Th26; reconsider G2 = RAT /\ as open Subset of (R^1 | (R^1 QQ)) by Th27; Q1 = G1 /\ the carrier of () proof thus Q1 c= G1 /\ the carrier of () :: according to XBOOLE_0:def 10 :: thesis: G1 /\ the carrier of () c= Q1 proof let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q1 or x in G1 /\ the carrier of () ) assume x in Q1 ; :: thesis: x in G1 /\ the carrier of () then consider q being Element of RAT such that A6: x = q and A7: q in rng f and A8: q < r ; q in by ; then q in G1 by XBOOLE_0:def 4; hence x in G1 /\ the carrier of () by ; :: thesis: verum end; let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G1 /\ the carrier of () or x in Q1 ) assume A9: x in G1 /\ the carrier of () ; :: thesis: x in Q1 then A10: x in the carrier of () by XBOOLE_0:def 4; A11: x in G1 by ; then reconsider x = x as Element of RAT by XBOOLE_0:def 4; x in by ; then x < r by XXREAL_1:233; hence x in Q1 by ; :: thesis: verum end; hence Q1 is open by TSP_1:def 1; :: thesis: ( Q2 is open & [#] () = Q1 \/ Q2 ) Q2 = G2 /\ the carrier of () proof thus Q2 c= G2 /\ the carrier of () :: according to XBOOLE_0:def 10 :: thesis: G2 /\ the carrier of () c= Q2 proof let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q2 or x in G2 /\ the carrier of () ) assume x in Q2 ; :: thesis: x in G2 /\ the carrier of () then consider q being Element of RAT such that A12: x = q and A13: q in rng f and A14: q > r ; q in by ; then q in G2 by XBOOLE_0:def 4; hence x in G2 /\ the carrier of () by ; :: thesis: verum end; let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G2 /\ the carrier of () or x in Q2 ) assume A15: x in G2 /\ the carrier of () ; :: thesis: x in Q2 then A16: x in the carrier of () by XBOOLE_0:def 4; A17: x in G2 by ; then reconsider x = x as Element of RAT by XBOOLE_0:def 4; x in by ; then x > r by XXREAL_1:235; hence x in Q2 by ; :: thesis: verum end; hence Q2 is open by TSP_1:def 1; :: thesis: [#] () = Q1 \/ Q2 thus Q1 \/ Q2 = [#] () :: thesis: verum proof thus Q1 \/ Q2 c= [#] () ; :: according to XBOOLE_0:def 10 :: thesis: [#] () c= Q1 \/ Q2 let x be Element of (); :: according to LATTICE7:def 1 :: thesis: ( not x in [#] () or x in Q1 \/ Q2 ) assume A18: x in [#] () ; :: thesis: x in Q1 \/ Q2 ( x < r or x > r ) by ; 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; coherence proof end; end; theorem Th28: :: 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 proof end; theorem Th29: :: BORSUK_7:39 for a, b being Real for f being continuous Function of (),R^1 for g being PartFunc of REAL,REAL st a <= b & f = g holds g is continuous proof end; definition let s be Point of R^1; let r be Real; :: original: + redefine func s + r -> Point of R^1; coherence s + r is Point of R^1 by ; end; definition let s be Point of R^1; let r be Real; :: original: - redefine func s - r -> Point of R^1; coherence s - r is Point of R^1 by ; end; definition let X be set ; let f be Function of X,R^1; let r be Real; :: original: + redefine func f + r -> Function of X,R^1; coherence r + f is Function of X,R^1 proof end; end; definition let X be set ; let f be Function of X,R^1; let r be Real; :: original: - redefine func f - r -> Function of X,R^1; coherence f - r is Function of X,R^1 proof end; end; definition let s, t be Point of R^1; let f be Path of s,t; let r be Real; :: original: + redefine func f + r -> Path of s + r,t + r; coherence r + f is Path of s + r,t + r proof end; :: original: - redefine func f - r -> Path of s - r,t - r; coherence f - r is Path of s - r,t - r proof end; end; definition func c[100] -> Point of () equals :: BORSUK_7:def 2 |[1,0,0]|; coherence |[1,0,0]| is Point of () proof end; end; :: deftheorem defines c[100] BORSUK_7:def 2 : c[100] = |[1,0,0]|; reconsider c100 = c[100] as Point of () ; reconsider c100a = c[100] as Point of (Tunit_circle (2 + 1)) ; definition func c[-100] -> Point of () equals :: BORSUK_7:def 3 |[(- 1),0,0]|; coherence |[(- 1),0,0]| is Point of () proof end; end; :: deftheorem defines c[-100] BORSUK_7:def 3 : c[-100] = |[(- 1),0,0]|; reconsider mc100 = c[-100] as Point of () ; theorem Th30: :: BORSUK_7:40 proof end; theorem :: BORSUK_7:41 theorem :: BORSUK_7:42 proof end; theorem :: BORSUK_7:43 for p being Point of () holds ( p 1 = |.p.| * (cos (Arg p)) & p 2 = |.p.| * (sin (Arg p)) ) proof end; theorem :: BORSUK_7:44 for p being Point of () holds p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * <i>)) proof end; theorem Th35: :: BORSUK_7:45 for i being Integer for p1, p2 being Point of () st |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) holds p1 = p2 proof end; set CM = CircleMap ; theorem Th36: :: BORSUK_7:46 for r being Real for p being Point of () st p = CircleMap . r holds Arg p = (2 * PI) * (frac r) proof end; theorem Th37: :: BORSUK_7:47 for p1, p2 being Point of () for u1, u2 being Point of () st u1 = p1 & u2 = p2 holds () . (u1,u2) = sqrt (((((p1 1) - (p2 1)) ^2) + (((p1 2) - (p2 2)) ^2)) + (((p1 3) - (p2 3)) ^2)) proof end; theorem Th38: :: BORSUK_7:48 for r being Real for p being Point of () for e being Point of () 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))).[,)) c= Ball (e,r) proof end; theorem Th39: :: BORSUK_7:49 for i being Integer for c being Complex for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) proof end; theorem :: BORSUK_7:50 for i being Integer for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i)) proof end; theorem Th41: :: BORSUK_7:51 for s being Real for p being Point of () holds |.(() . p).| = |.p.| proof end; theorem Th42: :: BORSUK_7:52 for s being Real for p being Point of () holds Arg (() . p) = Arg (Rotate ((),s)) proof end; theorem Th43: :: BORSUK_7:53 for s being Real for p being Point of () st p <> 0. () holds ex i being Integer st Arg (() . p) = (s + (Arg p)) + ((2 * PI) * i) proof end; theorem Th44: :: BORSUK_7:54 for s being Real holds () . (0. ()) = 0. () proof end; theorem Th45: :: BORSUK_7:55 for s being Real for p being Point of () st () . p = 0. () holds p = 0. () proof end; theorem Th46: :: BORSUK_7:56 for s being Real for p being Point of () holds () . ((Rotate (- s)) . p) = p proof end; theorem :: BORSUK_7:57 for s being Real holds () * (Rotate (- s)) = id () proof end; theorem Th48: :: BORSUK_7:58 for r, s being Real for p being Point of () holds ( p in Sphere ((0. ()),r) iff () . p in Sphere ((0. ()),r) ) proof end; theorem Th49: :: BORSUK_7:59 for r being non negative Real for s being Real holds () .: (Sphere ((0. ()),r)) = Sphere ((0. ()),r) proof end; definition let r be non negative Real; let s be Real; func RotateCircle (r,s) -> Function of (Tcircle ((0. ()),r)),(Tcircle ((0. ()),r)) equals :: BORSUK_7:def 4 () | (Tcircle ((0. ()),r)); coherence () | (Tcircle ((0. ()),r)) is Function of (Tcircle ((0. ()),r)),(Tcircle ((0. ()),r)) proof end; end; :: deftheorem defines RotateCircle BORSUK_7:def 4 : for r being non negative Real for s being Real holds RotateCircle (r,s) = () | (Tcircle ((0. ()),r)); registration let r be non negative Real; let s be Real; coherence RotateCircle (r,s) is being_homeomorphism proof end; end; theorem Th50: :: BORSUK_7:60 for r1, r2 being Real for p being Point of () st p = CircleMap . r2 holds (RotateCircle (1,(- (Arg p)))) . () = CircleMap . (r1 - r2) proof end; definition let n be non zero Nat; let p be Point of (); let r be non negative Real; func CircleIso (p,r) -> Function of (),(Tcircle (p,r)) means :Def5: :: BORSUK_7:def 5 for a being Point of () for b being Point of () st a = b holds it . a = (r * b) + p; existence ex b1 being Function of (),(Tcircle (p,r)) st for a being Point of () for b being Point of () st a = b holds b1 . a = (r * b) + p proof end; uniqueness for b1, b2 being Function of (),(Tcircle (p,r)) st ( for a being Point of () for b being Point of () st a = b holds b1 . a = (r * b) + p ) & ( for a being Point of () for b being Point of () st a = b holds b2 . a = (r * b) + p ) holds b1 = b2 proof end; end; :: deftheorem Def5 defines CircleIso BORSUK_7:def 5 : for n being non zero Nat for p being Point of () for r being non negative Real for b4 being Function of (),(Tcircle (p,r)) holds ( b4 = CircleIso (p,r) iff for a being Point of () for b being Point of () st a = b holds b4 . a = (r * b) + p ); registration let n be non zero Nat; let p be Point of (); let r be positive Real; coherence CircleIso (p,r) is being_homeomorphism proof end; end; definition func SphereMap -> Function of R^1,() means :Def6: :: BORSUK_7:def 6 for x being Real holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|; existence ex b1 being Function of R^1,() st for x being Real holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| proof end; uniqueness for b1, b2 being Function of R^1,() st ( for x being Real holds b1 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) & ( for x being Real holds b2 . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) holds b1 = b2 proof end; end; :: deftheorem Def6 defines SphereMap BORSUK_7:def 6 : for b1 being Function of R^1,() holds ( b1 = SphereMap iff for x being Real 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] proof end; Lm10: sin is Function of R^1,R^1 proof end; Lm11: cos is Function of R^1,R^1 proof end; Lm12: for r being Real holds SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| proof end; registration coherence proof end; end; definition let r be Real; func eLoop r -> Function of I[01],() means :Def7: :: BORSUK_7:def 7 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],() st for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| proof end; uniqueness for b1, b2 being Function of I[01],() 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 proof end; end; :: deftheorem Def7 defines eLoop BORSUK_7:def 7 : for r being Real for b2 being Function of I[01],() 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 Th52: :: BORSUK_7:62 for r being Real holds eLoop r = SphereMap * () proof end; definition let i be Integer; :: original: eLoop redefine func eLoop i -> Loop of c[100] ; coherence eLoop i is Loop of c[100] proof end; 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 proof end; end; theorem Th53: :: BORSUK_7:63 for n being Nat for p being Point of () st p <> 0. () holds |.(p (/) |.p.|).| = 1 proof end; definition let n be Nat; let p be Point of (); assume A1: p <> 0. () ; func Rn->S1 p -> Point of (Tcircle ((0. ()),1)) equals :Def8: :: BORSUK_7:def 8 p (/) |.p.|; coherence p (/) |.p.| is Point of (Tcircle ((0. ()),1)) proof end; end; :: deftheorem Def8 defines Rn->S1 BORSUK_7:def 8 : for n being Nat for p being Point of () st p <> 0. () 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)),(); 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)),() means :Def9: :: BORSUK_7:def 9 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)),() 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)) proof end; uniqueness for b1, b2 being Function of (Tunit_circle (n + 1)),() 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 proof end; end; :: deftheorem Def9 defines Sn1->Sn BORSUK_7:def 9 : for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),() for b3 being Function of (Tunit_circle (n + 1)),() 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 (); 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 :Def10: :: BORSUK_7:def 10 ( 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 ; 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 Def10 defines liftPath BORSUK_7:def 10 : for x0, y0 being Point of () 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 (); let r be Real; pred x,y are_antipodals_of p,r means :: BORSUK_7:def 11 ( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) ); end; :: deftheorem defines are_antipodals_of BORSUK_7:def 11 : for n being Nat for p, x, y being Point of () for r being Real 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 (); let r be Real; let f be Function; pred x,y are_antipodals_of p,r,f means :: BORSUK_7:def 12 ( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y ); end; :: deftheorem defines are_antipodals_of BORSUK_7:def 12 : for n being Nat for p, x, y being Point of () for r being Real 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 (); let r be Real; let f be Function of (Tcircle (p,r)),(); attr f is with_antipodals means :: BORSUK_7:def 13 ex x, y being Point of () st x,y are_antipodals_of p,r,f; end; :: deftheorem defines with_antipodals BORSUK_7:def 13 : for m, n being Nat for p being Point of () for r being Real for f being Function of (Tcircle (p,r)),() holds ( f is with_antipodals iff ex x, y being Point of () st x,y are_antipodals_of p,r,f ); notation let m, n be Nat; let p be Point of (); let r be Real; let f be Function of (Tcircle (p,r)),(); antonym without_antipodals f for with_antipodals ; end; theorem Th54: :: BORSUK_7:64 for n being non zero Nat for r being non negative Real for x being Point of () st x is Point of (Tcircle ((0. ()),r)) holds x, - x are_antipodals_of 0. (),r proof end; theorem Th55: :: BORSUK_7:65 for n being non zero Nat for p, x, y, x1, y1 being Point of () for r being positive Real st x,y are_antipodals_of 0. (),1 & x1 = (CircleIso (p,r)) . x & y1 = (CircleIso (p,r)) . y holds x1,y1 are_antipodals_of p,r proof end; theorem Th56: :: BORSUK_7:66 for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),() for x being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st f is without_antipodals holds (f . x) - (f . (- x)) <> 0. () proof end; theorem Th57: :: BORSUK_7:67 for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),() st f is without_antipodals holds Sn1->Sn f is odd proof end; theorem Th58: :: BORSUK_7:68 for n being non zero Nat for f, g, B1 being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),() st g = f (-) & B1 = f <--> g & f is without_antipodals holds Sn1->Sn f = B1 </> (() * B1) proof end; Lm13: for n being non zero Nat for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),() st f is without_antipodals & f is continuous holds Sn1->Sn f is continuous proof end; deffunc H1( Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),()) -> Element of bool [: the carrier of I[01], the carrier of ():] = (Sn1->Sn$1) * ();

Lm14: for s being Real
for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),() st f is without_antipodals & 0 <= s & s <= 1 / 2 holds
H1(f) . (s + (1 / 2)) = - (H1(f) . s)

proof end;

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 = - () holds ex I being odd Integer st S1[a,b,I] let a, b be Point of R^1; :: thesis: ( CircleMap . a = - () implies ex I being odd Integer st S1[a,b,I] ) assume A1: CircleMap . a = - () ; :: 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 .= cos (PI + ((2 * PI) * b)) by SIN_COS:79 ; sin ((2 * PI) * a) = - (sin ((2 * PI) * b)) by .= 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 ; 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)),() st f is without_antipodals & f is continuous holds H1(f) is nullhomotopic Loop of () . c100a proof end; Lm17: now :: thesis: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),() for s being Real for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {(() . c[100])} & 0 <= s & s <= 1 / 2 holds ex IT being odd Integer st for L being Loop of () . 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)),(); :: thesis: for s being Real for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {(() . c[100])} & 0 <= s & s <= 1 / 2 holds ex IT being odd Integer st for L being Loop of () . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (IT / 2) let s be Real; :: thesis: for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {(() . c[100])} & 0 <= s & s <= 1 / 2 holds ex IT being odd Integer st for L being Loop of () . 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 " {(() . c[100])} & 0 <= s & s <= 1 / 2 implies ex IT being odd Integer st for L being Loop of () . 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 " {(() . c[100])} and A3: ( 0 <= s & s <= 1 / 2 ) ; :: thesis: ex IT being odd Integer st for L being Loop of () . 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 () . 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 ; reconsider L = H1(f) as Loop of () . c100a by ; 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 ; A4: H1(f) = CircleMap * (liftPath (L,xt)) by ; ( (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 () . c100a st L = H1(f) holds (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (I / 2) thus for L being Loop of () . 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)),(), set , Integer] means for L being Loop of (Sn1->Sn$1) . c100a st L = H1($1) holds for s being Real 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)),()
for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {(() . 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)),(); :: thesis: for xt being set st f is without_antipodals & f is continuous & xt in CircleMap " {(() . 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 " {(() . 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 " {(() . c[100])} ; :: thesis: ex I being odd Integer st S2[f,xt,I]
reconsider L1 = H1(f) as Loop of () . c100a by ;
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 object ; :: according to TARSKI: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 object 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 by A6;
A8: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . x = (AffineMap (1,(1 / 2))) . x by
.= (1 * x) + (1 / 2) by FCONT_1:def 4 ;
( 0 <= x & x <= 1 / 2 ) by ;
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 ; :: 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
.= [.0,(1 / 2).] by ;
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 ;
consider ITj0 being odd Integer such that
A11: for L being Loop of () . 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 () . c100a; :: thesis: ( L = H1(f) implies for s being Real 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 st 0 <= s & s <= 1 / 2 holds
(liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2)

let s be Real; :: 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 ;
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
.= (1 * s) + (1 / 2) by FCONT_1:def 4 ;
consider ITs being odd Integer such that
A18: for L being Loop of () . 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
.= 2 * (((liftPath (L1,xt)) . (1 / 2)) - ((liftPath (L1,xt)) . 0)) by
.= 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
.= 2 * (((liftPath (L1,xt)) . (s + (1 / 2))) - ((liftPath (L1,xt)) . s)) by
.= 2 * (ITs / 2) by A20 ;
A23: rng W c= INT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng W or y in INT )
assume y in rng W ; :: thesis:
then consider s being object such that
A24: s in dom W and
A25: W . s = y by FUNCT_1:def 3;
reconsider s = s as Real by A24;
A26: ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) . s = (AffineMap (1,(1 / 2))) . s by
.= (1 * s) + (1 / 2) by FCONT_1:def 4 ;
( 0 <= s & s <= 1 / 2 ) by ;
then consider ITs being odd Integer such that
A27: for L being Loop of () . 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
.= 2 * (((liftPath (L1,xt)) . (s + (1 / 2))) - ((liftPath (L1,xt)) . s)) by
.= 2 * (ITs / 2) by A28 ;
hence y in INT by ; :: 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 ;
reconsider SR = RAT as Subset of R^1 by ;
reconsider W1 = W as Function of (Closed-Interval-TSpace (0,(1 / 2))),(R^1 | SR) by ;
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 ;
reconsider f1 = R^1 ((AffineMap (1,(1 / 2))) | [.0,(1 / 2).]) as Function of (Closed-Interval-TSpace (0,(1 / 2))),I[01] by ;
rng (liftPath (L1,xt)) c= REAL by TOPMETR:17;
then reconsider ll1 = liftPath (L1,xt) as PartFunc of REAL,REAL by ;
liftPath (L1,xt) is continuous by ;
then A33: ll1 is continuous by ;
(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 ;
R^1 W is continuous ;
then W1 is continuous by ;
then W1 is constant by ;
hence (liftPath (L,xt)) . (s + (1 / 2)) = ((liftPath (L,xt)) . s) + (ITj0 / 2) by A20, A12, A21, A22, A9, A10, A15, A14; :: thesis: verum
end;
end;

Lm19: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),()
for xt being Point of R^1
for L being Loop of () . 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

proof end;

Lm20: for f being Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),() st f is without_antipodals & f is continuous holds
not H1(f) is nullhomotopic Loop of () . c100a

proof end;

Lm21: for f being continuous Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),() holds f is with_antipodals
proof end;

registration
let n be non zero Nat;
let r be negative Real;
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 ():];
coherence
for b1 being Function of (Tcircle (p,r)),() holds b1 is without_antipodals
proof end;
end;

:: Borsuk-Ulam Theorem
registration
let r be non negative Real;
let p be Point of ();
cluster Function-like quasi_total continuous -> with_antipodals for Element of bool [: the carrier of (Tcircle (p,r)), the carrier of ():];
coherence
for b1 being Function of (Tcircle (p,r)),() st b1 is continuous holds
b1 is with_antipodals
proof end;
end;