:: BORSUK_7 semantic presentation
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
proof
let r, s be real number ; ::_thesis: ( 0 <= r & 0 <= s & r ^2 = s ^2 implies r = s )
assume that
A1: 0 <= r and
A2: 0 <= s and
A3: r ^2 = s ^2 and
A4: r <> s ; ::_thesis: contradiction
- Q >= - (- s) by A1, A3, A4, SQUARE_1:40;
hence contradiction by A4, A2, A3, SQUARE_1:40; ::_thesis: verum
end;
theorem Th2: :: BORSUK_7:2
for r, s being real number st frac r >= frac s holds
frac (r - s) = (frac r) - (frac s)
proof
let r, s be real number ; ::_thesis: ( frac r >= frac s implies frac (r - s) = (frac r) - (frac s) )
assume A1: frac r >= frac s ; ::_thesis: frac (r - s) = (frac r) - (frac s)
set a = ((r - s) - (frac r)) + (frac s);
A2: ((r - s) - (frac r)) + (frac s) = (r - (frac r)) - (s - (frac s)) ;
A3: ((r - s) - (frac r)) + (frac s) = (r - s) + ((- (frac r)) + (frac s)) ;
- (frac r) <= - (frac s) by A1, XREAL_1:24;
then (- (frac r)) + (frac s) <= (- (frac s)) + (frac s) by XREAL_1:6;
then A4: ((r - s) - (frac r)) + (frac s) <= (r - s) + Q by A3, XREAL_1:6;
A5: ((r - s) - (frac r)) + (frac s) = (r - s) - ((frac r) - (frac s)) ;
A6: 0 <= frac s by INT_1:43;
frac r < 1 by INT_1:43;
then 1 + (frac s) > (frac r) + Q by A6, XREAL_1:8;
then 1 > (frac r) - (frac s) by XREAL_1:19;
then (r - s) - 1 < ((r - s) - (frac r)) + (frac s) by A5, XREAL_1:10;
then ((r - s) - (frac r)) + (frac s) = [\(r - s)/] by A4, A2, INT_1:def_6;
hence frac (r - s) = (frac r) - (frac s) ; ::_thesis: verum
end;
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
proof
let r, s be real number ; ::_thesis: ( frac r < frac s implies frac (r - s) = ((frac r) - (frac s)) + 1 )
assume A1: frac r < frac s ; ::_thesis: frac (r - s) = ((frac r) - (frac s)) + 1
set a = (((r - s) - (frac r)) + (frac s)) - 1;
A2: (((r - s) - (frac r)) + (frac s)) - 1 = ((r - (frac r)) - (s - (frac s))) - 1 ;
A3: (((r - s) - (frac r)) + (frac s)) - 1 = (r - s) + (((- (frac r)) + (frac s)) - 1) ;
frac s < 1 by INT_1:43;
then A4: (frac s) - 1 < 1 - 1 by XREAL_1:9;
0 <= frac r by INT_1:43;
then ((frac s) - 1) - (frac r) <= (frac r) - (frac r) by A4;
then A5: (((r - s) - (frac r)) + (frac s)) - 1 <= (r - s) + Q by A3, XREAL_1:6;
A6: (((r - s) - (frac r)) + (frac s)) - 1 = ((r - s) - 1) - ((frac r) - (frac s)) ;
(frac r) - (frac r) > (frac r) - (frac s) by A1, XREAL_1:10;
then ((r - s) - 1) - Q < (((r - s) - (frac r)) + (frac s)) - 1 by A6, XREAL_1:10;
then (((r - s) - (frac r)) + (frac s)) - 1 = [\(r - s)/] by A5, A2, INT_1:def_6;
hence frac (r - s) = ((frac r) - (frac s)) + 1 ; ::_thesis: verum
end;
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 ) )
proof
let r, s be real number ; ::_thesis: ex i being Integer st
( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) )
( frac (r - s) = ((frac r) - (frac s)) + Q or frac (r - s) = ((frac r) - (frac s)) + 1 ) by Th2, Th3;
hence ex i being Integer st
( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) ) ; ::_thesis: verum
end;
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))/]) )
proof
let r be real number ; ::_thesis: ( not sin r = 0 or r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) )
set i = [\(r / (2 * PI))/];
assume A1: sin r = 0 ; ::_thesis: ( r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) )
consider w being real number such that
A2: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + r and
A3: 0 <= w and
A4: w < 2 * PI by COMPLEX2:1;
sin w = sin r by A2, COMPLEX2:8;
then ( w = 0 or w = PI ) by A1, A3, A4, COMPTRIG:17;
hence ( r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) by A2; ::_thesis: verum
end;
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))/]) )
proof
let r be real number ; ::_thesis: ( not cos r = 0 or r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) )
set i = [\(r / (2 * PI))/];
assume A1: cos r = 0 ; ::_thesis: ( r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) )
consider w being real number such that
A2: w = ((2 * PI) * (- [\(r / (2 * PI))/])) + r and
A3: 0 <= w and
A4: w < 2 * PI by COMPLEX2:1;
cos w = cos r by A2, COMPLEX2:9;
then ( w = PI / 2 or w = (3 * PI) / 2 ) by A1, A3, A4, COMPTRIG:18;
hence ( r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) ) by A2; ::_thesis: verum
end;
theorem Th7: :: BORSUK_7:7
for r being real number st sin r = 0 holds
ex i being Integer st r = PI * i
proof
let r be real number ; ::_thesis: ( sin r = 0 implies ex i being Integer st r = PI * i )
assume sin r = 0 ; ::_thesis: ex i being Integer st r = PI * i
then ( r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) by Th5;
then ( r = PI * (2 * [\(r / (2 * PI))/]) or r = PI * (1 + (2 * [\(r / (2 * PI))/])) ) ;
hence ex i being Integer st r = PI * i ; ::_thesis: verum
end;
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)
proof
let r be real number ; ::_thesis: ( cos r = 0 implies ex i being Integer st r = (PI / 2) + (PI * i) )
assume cos r = 0 ; ::_thesis: ex i being Integer st r = (PI / 2) + (PI * i)
then ( r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) or r = ((3 * PI) / 2) + ((2 * PI) * [\(r / (2 * PI))/]) ) by Th6;
then ( r = (PI / 2) + (PI * (2 * [\(r / (2 * PI))/])) or r = (PI / 2) + (PI * (1 + (2 * [\(r / (2 * PI))/]))) ) ;
hence ex i being Integer st r = (PI / 2) + (PI * i) ; ::_thesis: verum
end;
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) )
proof
let r, s be real number ; ::_thesis: ( sin r = sin s implies ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) )
assume A1: sin r = sin s ; ::_thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) )
A2: (sin r) - (sin s) = 2 * ((cos ((r + s) / 2)) * (sin ((r - s) / 2))) by SIN_COS4:16;
percases ( sin ((r - s) / 2) = 0 or cos ((r + s) / 2) = 0 ) by A1, A2;
suppose sin ((r - s) / 2) = 0 ; ::_thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) )
hence ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) by Lm5; ::_thesis: verum
end;
suppose cos ((r + s) / 2) = 0 ; ::_thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) )
then consider i being Integer such that
A3: (r + s) / 2 = (PI / 2) + (PI * i) by Th8;
r = (PI - s) + ((2 * PI) * i) by A3;
hence ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) ; ::_thesis: verum
end;
end;
end;
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) )
proof
let r, s be real number ; ::_thesis: ( cos r = cos s implies ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) )
assume A1: cos r = cos s ; ::_thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )
A2: (cos r) - (cos s) = - (2 * ((sin ((r + s) / 2)) * (sin ((r - s) / 2)))) by SIN_COS4:18;
percases ( sin ((r - s) / 2) = 0 or sin ((r + s) / 2) = 0 ) by A1, A2;
suppose sin ((r - s) / 2) = 0 ; ::_thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )
hence ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) by Lm5; ::_thesis: verum
end;
suppose sin ((r + s) / 2) = 0 ; ::_thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )
then consider i being Integer such that
A3: (r + s) / 2 = PI * i by Th7;
(r + s) - s = ((2 * PI) * i) - s by A3;
hence ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) ) ; ::_thesis: verum
end;
end;
end;
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)
proof
let r, s be real number ; ::_thesis: ( sin r = sin s & cos r = cos s implies ex i being Integer st r = s + ((2 * PI) * i) )
assume that
A1: sin r = sin s and
A2: cos r = cos s ; ::_thesis: ex i being Integer st r = s + ((2 * PI) * i)
consider i being Integer such that
A3: ( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) by A1, Th9;
consider j being Integer such that
A4: ( r = s + ((2 * PI) * j) or r = (- s) + ((2 * PI) * j) ) by A2, Th10;
percases ( r = s + ((2 * PI) * i) or r = s + ((2 * PI) * j) or ( r = (PI - s) + ((2 * PI) * i) & r = (- s) + ((2 * PI) * j) ) ) by A3, A4;
suppose ( r = s + ((2 * PI) * i) or r = s + ((2 * PI) * j) ) ; ::_thesis: ex i being Integer st r = s + ((2 * PI) * i)
hence ex i being Integer st r = s + ((2 * PI) * i) ; ::_thesis: verum
end;
suppose ( r = (PI - s) + ((2 * PI) * i) & r = (- s) + ((2 * PI) * j) ) ; ::_thesis: ex i being Integer st r = s + ((2 * PI) * i)
then PI / PI = (PI * (2 * (j - i))) / PI ;
then PI / PI = 2 * (j - i) by XCMPLX_1:89;
then 1 = 2 * (j - i) by XCMPLX_1:60;
then j - i = 1 / 2 ;
hence ex i being Integer st r = s + ((2 * PI) * i) by NAT_D:33; ::_thesis: verum
end;
end;
end;
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
proof
let i be Integer; ::_thesis: for c1, c2 being complex number st |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) holds
c1 = c2
let c1, c2 be complex number ; ::_thesis: ( |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) implies c1 = c2 )
assume A1: ( |.c1.| = |.c2.| & Arg c1 = (Arg c2) + ((2 * PI) * i) ) ; ::_thesis: c1 = c2
A2: ( cos (Arg c2) = cos ((Arg c2) + ((2 * PI) * i)) & sin (Arg c2) = sin ((Arg c2) + ((2 * PI) * i)) ) by COMPLEX2:8, COMPLEX2:9;
( c1 = (|.c1.| * (cos (Arg c1))) + ((|.c1.| * (sin (Arg c1))) * *) & c2 = (|.c2.| * (cos (Arg c2))) + ((|.c2.| * (sin (Arg c2))) * **) ) by COMPTRIG:62;
hence c1 = c2 by A1, A2; ::_thesis: verum
end;
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
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom (f + c) or not b1 in dom (f + c) or not (f + c) . x = (f + c) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom (f + c) or not y in dom (f + c) or not (f + c) . x = (f + c) . y or x = y )
assume that
A1: ( x in dom (f + c) & y in dom (f + c) ) and
A2: (f + c) . x = (f + c) . y ; ::_thesis: x = y
A3: dom (f + c) = dom f by VALUED_1:def_2;
( (f + c) . x = (f . x) + c & (f + c) . y = (f . y) + c ) by A1, VALUED_1:def_2;
hence x = y by A1, A3, A2, FUNCT_1:def_4; ::_thesis: verum
end;
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
proof
let f be complex-valued FinSequence; ::_thesis: len (- f) = len f
Seg (len (- f)) = dom (- f) by FINSEQ_1:def_3
.= dom f by VALUED_1:def_5
.= Seg (len f) by FINSEQ_1:def_3 ;
hence len (- f) = len f by FINSEQ_1:6; ::_thesis: verum
end;
theorem Th14: :: BORSUK_7:14
for n being Nat holds - (0* n) = 0* n
proof
let n be Nat; ::_thesis: - (0* n) = 0* n
set f = 0* n;
set g = - (0* n);
thus len (0* n) = len (- (0* n)) by Th13; :: according to FINSEQ_1:def_17 ::_thesis: for b1 being set holds
( not 1 <= b1 or not b1 <= len (- (0* n)) or (- (0* n)) . b1 = (0* n) . b1 )
let k be Nat; ::_thesis: ( not 1 <= k or not k <= len (- (0* n)) or (- (0* n)) . k = (0* n) . k )
assume ( 1 <= k & k <= len (- (0* n)) ) ; ::_thesis: (- (0* n)) . k = (0* n) . k
A1: (0* n) . k = 0 ;
thus (0* n) . k = - Q
.= (- (0* n)) . k by A1, VALUED_1:8 ; ::_thesis: verum
end;
theorem Th15: :: BORSUK_7:15
for n being Nat
for f being complex-valued Function st f <> 0* n holds
- f <> 0* n
proof
let n be Nat; ::_thesis: for f being complex-valued Function st f <> 0* n holds
- f <> 0* n
let f be complex-valued Function; ::_thesis: ( f <> 0* n implies - f <> 0* n )
assume A1: f <> 0* n ; ::_thesis: - f <> 0* n
assume - f = 0* n ; ::_thesis: contradiction
then - (- f) = - (0* n) ;
hence contradiction by A1, Th14; ::_thesis: verum
end;
theorem Th16: :: BORSUK_7:16
for r1, r2, r3 being real number holds sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*>
proof
let r1, r2, r3 be real number ; ::_thesis: sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*>
A1: ( r1 in REAL & r2 in REAL & r3 in REAL ) by XREAL_0:def_1;
( <*r1,r2*> is FinSequence of REAL & <*r3*> is FinSequence of REAL ) by TOPREALC:19;
hence sqr <*r1,r2,r3*> = (sqr <*r1,r2*>) ^ (sqr <*r3*>) by TOPREAL7:10
.= <*(r1 ^2),(r2 ^2)*> ^ (sqr <*r3*>) by A1, TOPREAL6:11
.= <*(r1 ^2),(r2 ^2),(r3 ^2)*> by RVSUM_1:55 ;
::_thesis: verum
end;
theorem Th17: :: BORSUK_7:17
for r1, r2, r3 being real number holds Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2)
proof
let r1, r2, r3 be real number ; ::_thesis: Sum (sqr <*r1,r2,r3*>) = ((r1 ^2) + (r2 ^2)) + (r3 ^2)
thus Sum (sqr <*r1,r2,r3*>) = Sum <*(r1 ^2),(r2 ^2),(r3 ^2)*> by Th16
.= ((r1 ^2) + (r2 ^2)) + (r3 ^2) by RVSUM_1:78 ; ::_thesis: verum
end;
theorem Th18: :: BORSUK_7:18
for c being complex number
for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2)
proof
let c be complex number ; ::_thesis: for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2)
let f be complex-valued FinSequence; ::_thesis: (c (#) f) ^2 = (c ^2) (#) (f ^2)
A1: dom ((c (#) f) ^2) = dom (c (#) f) by VALUED_1:11
.= dom f by VALUED_1:def_5 ;
A2: dom ((c ^2) (#) (f ^2)) = dom (f ^2) by VALUED_1:def_5
.= dom f by VALUED_1:11 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_((c_(#)_f)_^2)_holds_
((c_(#)_f)_^2)_._x_=_((c_^2)_(#)_(f_^2))_._x
let x be set ; ::_thesis: ( x in dom ((c (#) f) ^2) implies ((c (#) f) ^2) . x = ((c ^2) (#) (f ^2)) . x )
assume x in dom ((c (#) f) ^2) ; ::_thesis: ((c (#) f) ^2) . x = ((c ^2) (#) (f ^2)) . x
thus ((c (#) f) ^2) . x = ((c (#) f) . x) ^2 by VALUED_1:11
.= (c * (f . x)) ^2 by VALUED_1:6
.= (c ^2) * ((f . x) ^2)
.= (c ^2) * ((f ^2) . x) by VALUED_1:11
.= ((c ^2) (#) (f ^2)) . x by VALUED_1:6 ; ::_thesis: verum
end;
hence (c (#) f) ^2 = (c ^2) (#) (f ^2) by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
theorem Th19: :: BORSUK_7:19
for c being complex number
for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2)
proof
let c be complex number ; ::_thesis: for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2)
let f be complex-valued FinSequence; ::_thesis: (f (/) c) ^2 = (f ^2) (/) (c ^2)
thus (f (/) c) ^2 = ((1 / c) ^2) (#) (f ^2) by Th18
.= ((1 * 1) / (c * c)) (#) (f ^2) by XCMPLX_1:76
.= (f ^2) (/) (c ^2) ; ::_thesis: verum
end;
theorem Th20: :: BORSUK_7:20
for f being real-valued FinSequence st Sum f <> 0 holds
Sum (f (/) (Sum f)) = 1
proof
let f be real-valued FinSequence; ::_thesis: ( Sum f <> 0 implies Sum (f (/) (Sum f)) = 1 )
Sum (f (/) (Sum f)) = (Sum f) / (Sum f) by RVSUM_1:87;
hence ( Sum f <> 0 implies Sum (f (/) (Sum f)) = 1 ) by XCMPLX_1:60; ::_thesis: verum
end;
Lm6: 1,2,3 are_mutually_different
proof
thus ( 1 <> 2 & 1 <> 3 & 2 <> 3 ) ; :: according to ZFMISC_1:def_5 ::_thesis: verum
end;
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}
proof
let a, b, x, y, z be set ; ::_thesis: for c being complex number holds rng ((a,b,c) --> (x,y,z)) c= {x,y,z}
let c be complex number ; ::_thesis: rng ((a,b,c) --> (x,y,z)) c= {x,y,z}
A1: {x,y} \/ {z} = {x,y,z} by ENUMSET1:3;
A2: rng ((a,b,c) --> (x,y,z)) c= (rng ((a,b) --> (x,y))) \/ (rng (c .--> z)) by FUNCT_4:17;
A3: rng (c .--> z) = {z} by FUNCOP_1:8;
rng ((a,b) --> (x,y)) c= {x,y} by FUNCT_4:62;
then (rng ((a,b) --> (x,y))) \/ (rng (c .--> z)) c= {x,y} \/ {z} by A3, XBOOLE_1:13;
hence rng ((a,b,c) --> (x,y,z)) c= {x,y,z} by A2, A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: BORSUK_7:23
for a, x, y, z being set holds (a,a,a) --> (x,y,z) = a .--> z
proof
let a, x, y, z be set ; ::_thesis: (a,a,a) --> (x,y,z) = a .--> z
thus (a,a,a) --> (x,y,z) = (a,a) --> (y,z) by FUNCT_4:81
.= a .--> z by FUNCT_4:81 ; ::_thesis: verum
end;
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)
proof
let a, b, x, y, z be set ; ::_thesis: ( a <> b implies (a,b,a) --> (x,y,z) = (a,b) --> (z,y) )
assume A1: a <> b ; ::_thesis: (a,b,a) --> (x,y,z) = (a,b) --> (z,y)
A2: dom ((a,b,a) --> (x,y,z)) = {a,b,a} by BVFUNC14:11
.= {a,a,b} by ENUMSET1:57
.= {a,b} by ENUMSET1:30 ;
hence dom ((a,b,a) --> (x,y,z)) = dom ((a,b) --> (z,y)) by FUNCT_4:62; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((a,b,a) --> (x,y,z)) or ((a,b,a) --> (x,y,z)) . b1 = ((a,b) --> (z,y)) . b1 )
let k be set ; ::_thesis: ( not k in dom ((a,b,a) --> (x,y,z)) or ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k )
assume A3: k in dom ((a,b,a) --> (x,y,z)) ; ::_thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k
percases ( k = a or k = b ) by A2, A3, TARSKI:def_2;
supposeA4: k = a ; ::_thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k
hence ((a,b,a) --> (x,y,z)) . k = z by FUNCT_4:89
.= ((a,b) --> (z,y)) . k by A1, A4, FUNCT_4:63 ;
::_thesis: verum
end;
supposeA5: k = b ; ::_thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k
thus ((a,b,a) --> (x,y,z)) . k = ((a .--> x) +* ((b,a) --> (y,z))) . k by FUNCT_4:14
.= y by A1, A5, FUNCT_4:84
.= ((a,b) --> (z,y)) . k by A5, FUNCT_4:63 ; ::_thesis: verum
end;
end;
end;
theorem Th26: :: BORSUK_7:26
for a, b, x, y, z being set holds (a,b,b) --> (x,y,z) = (a,b) --> (x,z)
proof
let a, b, x, y, z be set ; ::_thesis: (a,b,b) --> (x,y,z) = (a,b) --> (x,z)
thus (a,b,b) --> (x,y,z) = (a .--> x) +* ((b,b) --> (y,z)) by FUNCT_4:14
.= (a,b) --> (x,z) by FUNCT_4:81 ; ::_thesis: verum
end;
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 )
proof
let a, b, x, y, z be set ; ::_thesis: 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 )
let c be complex number ; ::_thesis: ( a,b,c are_mutually_different implies ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z ) )
assume A1: a,b,c are_mutually_different ; ::_thesis: ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z )
set f = (a,b) --> (x,y);
set g = c .--> z;
set h = (a,b,c) --> (x,y,z);
A2: a <> b by A1, ZFMISC_1:def_5;
a <> c by A1, ZFMISC_1:def_5;
then A3: not a in {c} by TARSKI:def_1;
b <> c by A1, ZFMISC_1:def_5;
then A4: not b in {c} by TARSKI:def_1;
A5: c in {c} by TARSKI:def_1;
A6: dom (c .--> z) = {c} by FUNCOP_1:13;
hence ((a,b,c) --> (x,y,z)) . a = ((a,b) --> (x,y)) . a by A3, FUNCT_4:11
.= x by A2, FUNCT_4:63 ;
::_thesis: ( ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z )
thus ((a,b,c) --> (x,y,z)) . b = ((a,b) --> (x,y)) . b by A4, A6, FUNCT_4:11
.= y by FUNCT_4:63 ; ::_thesis: ((a,b,c) --> (x,y,z)) . c = z
thus ((a,b,c) --> (x,y,z)) . c = (c .--> z) . c by A5, A6, FUNCT_4:13
.= z by FUNCOP_1:72 ; ::_thesis: verum
end;
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)
proof
let a, b, x, y, z be set ; ::_thesis: 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)
let c be complex number ; ::_thesis: 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)
let f be Function; ::_thesis: ( dom f = {a,b,c} & f . a = x & f . b = y & f . c = z implies f = (a,b,c) --> (x,y,z) )
assume that
A1: dom f = {a,b,c} and
A2: ( f . a = x & f . b = y & f . c = z ) ; ::_thesis: f = (a,b,c) --> (x,y,z)
set g = (a,b,c) --> (x,y,z);
thus dom f = dom ((a,b,c) --> (x,y,z)) by A1, BVFUNC14:11; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom f or f . b1 = ((a,b,c) --> (x,y,z)) . b1 )
let k be set ; ::_thesis: ( not k in dom f or f . k = ((a,b,c) --> (x,y,z)) . k )
assume k in dom f ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k
then A3: ( k = a or k = b or k = c ) by A1, ENUMSET1:def_1;
percases ( a,b,c are_mutually_different or not a,b,c are_mutually_different ) ;
suppose a,b,c are_mutually_different ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k
hence f . k = ((a,b,c) --> (x,y,z)) . k by A2, A3, Th28; ::_thesis: verum
end;
supposeA4: not a,b,c are_mutually_different ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k
percases ( ( a = b & a <> c ) or a = c or ( b = c & a <> c ) ) by A4, ZFMISC_1:def_5;
supposeA5: ( a = b & a <> c ) ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k
then (a,b,c) --> (x,y,z) = (a,c) --> (y,z) by FUNCT_4:81;
hence f . k = ((a,b,c) --> (x,y,z)) . k by A5, A2, A3, FUNCT_4:63; ::_thesis: verum
end;
supposeA6: a = c ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k
percases ( a <> b or a = b ) ;
supposeA7: a <> b ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k
then (a,b,c) --> (x,y,z) = (a,b) --> (z,y) by A6, Th25;
hence f . k = ((a,b,c) --> (x,y,z)) . k by A6, A2, A3, A7, FUNCT_4:63; ::_thesis: verum
end;
suppose a = b ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k
hence f . k = ((a,b,c) --> (x,y,z)) . k by A6, A2, A3, FUNCOP_1:72; ::_thesis: verum
end;
end;
end;
supposeA8: ( b = c & a <> c ) ; ::_thesis: f . k = ((a,b,c) --> (x,y,z)) . k
then (a,b,c) --> (x,y,z) = (a,b) --> (x,z) by Th26;
hence f . k = ((a,b,c) --> (x,y,z)) . k by A8, A2, A3, FUNCT_4:63; ::_thesis: verum
end;
end;
end;
end;
end;
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)
proof
let a, b be set ; ::_thesis: for c being complex number holds <*a,b,c*> = (1,2,3) --> (a,b,c)
let c be complex number ; ::_thesis: <*a,b,c*> = (1,2,3) --> (a,b,c)
set f = (1,2,3) --> (a,b,c);
set g = <*a,b,c*>;
A1: dom <*a,b,c*> = Seg (len <*a,b,c*>) by FINSEQ_1:def_3
.= {1,2,3} by FINSEQ_3:1, FINSEQ_1:45 ;
A2: dom ((1,2,3) --> (a,b,c)) = {1,2,3} by BVFUNC14:11;
now__::_thesis:_for_x_being_set_st_x_in_dom_((1,2,3)_-->_(a,b,c))_holds_
((1,2,3)_-->_(a,b,c))_._x_=_<*a,b,c*>_._x
let x be set ; ::_thesis: ( x in dom ((1,2,3) --> (a,b,c)) implies ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1 )
assume A3: x in dom ((1,2,3) --> (a,b,c)) ; ::_thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1
percases ( x = 1 or x = 2 or x = 3 ) by A2, A3, ENUMSET1:def_1;
supposeA4: x = 1 ; ::_thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1
hence ((1,2,3) --> (a,b,c)) . x = a by Lm6, Th28
.= <*a,b,c*> . x by A4, FINSEQ_1:45 ;
::_thesis: verum
end;
supposeA5: x = 2 ; ::_thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1
hence ((1,2,3) --> (a,b,c)) . x = b by Lm6, Th28
.= <*a,b,c*> . x by A5, FINSEQ_1:45 ;
::_thesis: verum
end;
supposeA6: x = 3 ; ::_thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1
hence ((1,2,3) --> (a,b,c)) . x = c by Lm6, Th28
.= <*a,b,c*> . x by A6, FINSEQ_1:45 ;
::_thesis: verum
end;
end;
end;
hence <*a,b,c*> = (1,2,3) --> (a,b,c) by A1, BVFUNC14:11, FUNCT_1:2; ::_thesis: verum
end;
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))}
proof
let a, b, x, y, z be set ; ::_thesis: 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))}
let c be complex number ; ::_thesis: ( a,b,c are_mutually_different implies product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} )
assume A1: a,b,c are_mutually_different ; ::_thesis: product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))}
set X = {((a,b,c) --> (x,y,z))};
set f = (a,b,c) --> ({x},{y},{z});
A2: dom ((a,b,c) --> ({x},{y},{z})) = {a,b,c} by BVFUNC14:11;
now__::_thesis:_for_m_being_set_holds_
(_(_m_in_{((a,b,c)_-->_(x,y,z))}_implies_ex_g_being_Function_st_
(_m_=_g_&_dom_g_=_dom_((a,b,c)_-->_({x},{y},{z}))_&_(_for_x_being_set_st_x_in_dom_((a,b,c)_-->_({x},{y},{z}))_holds_
g_._x_in_((a,b,c)_-->_({x},{y},{z}))_._x_)_)_)_&_(_ex_g_being_Function_st_
(_m_=_g_&_dom_g_=_dom_((a,b,c)_-->_({x},{y},{z}))_&_(_for_x_being_set_st_x_in_dom_((a,b,c)_-->_({x},{y},{z}))_holds_
g_._x_in_((a,b,c)_-->_({x},{y},{z}))_._x_)_)_implies_m_in_{((a,b,c)_-->_(x,y,z))}_)_)
let m be set ; ::_thesis: ( ( m in {((a,b,c) --> (x,y,z))} implies ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) ) & ( ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) implies m in {((a,b,c) --> (x,y,z))} ) )
thus ( m in {((a,b,c) --> (x,y,z))} implies ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) ) ::_thesis: ( ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) ) implies m in {((a,b,c) --> (x,y,z))} )
proof
assume A3: m in {((a,b,c) --> (x,y,z))} ; ::_thesis: ex g being Function st
( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) )
take g = (a,b,c) --> (x,y,z); ::_thesis: ( m = g & dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) )
thus m = g by A3, TARSKI:def_1; ::_thesis: ( dom g = dom ((a,b,c) --> ({x},{y},{z})) & ( for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ) )
thus dom g = dom ((a,b,c) --> ({x},{y},{z})) by A2, BVFUNC14:11; ::_thesis: for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x
let k be set ; ::_thesis: ( k in dom ((a,b,c) --> ({x},{y},{z})) implies g . k in ((a,b,c) --> ({x},{y},{z})) . k )
assume k in dom ((a,b,c) --> ({x},{y},{z})) ; ::_thesis: g . k in ((a,b,c) --> ({x},{y},{z})) . k
then A4: ( k = a or k = b or k = c ) by A2, ENUMSET1:def_1;
( g . a = x & ((a,b,c) --> ({x},{y},{z})) . a = {x} & g . b = y & ((a,b,c) --> ({x},{y},{z})) . b = {y} & g . c = z & ((a,b,c) --> ({x},{y},{z})) . c = {z} ) by A1, Th28;
hence g . k in ((a,b,c) --> ({x},{y},{z})) . k by A4, TARSKI:def_1; ::_thesis: verum
end;
given g being Function such that A5: m = g and
A6: dom g = dom ((a,b,c) --> ({x},{y},{z})) and
A7: for x being set st x in dom ((a,b,c) --> ({x},{y},{z})) holds
g . x in ((a,b,c) --> ({x},{y},{z})) . x ; ::_thesis: m in {((a,b,c) --> (x,y,z))}
( a in dom ((a,b,c) --> ({x},{y},{z})) & b in dom ((a,b,c) --> ({x},{y},{z})) & c in dom ((a,b,c) --> ({x},{y},{z})) ) by A2, ENUMSET1:def_1;
then ( g . a in ((a,b,c) --> ({x},{y},{z})) . a & g . b in ((a,b,c) --> ({x},{y},{z})) . b & g . c in ((a,b,c) --> ({x},{y},{z})) . c & ((a,b,c) --> ({x},{y},{z})) . a = {x} & ((a,b,c) --> ({x},{y},{z})) . b = {y} & ((a,b,c) --> ({x},{y},{z})) . c = {z} ) by A1, A7, Th28;
then ( g . a = x & g . b = y & g . c = z ) by TARSKI:def_1;
then g = (a,b,c) --> (x,y,z) by A2, A6, Th29;
hence m in {((a,b,c) --> (x,y,z))} by A5, TARSKI:def_1; ::_thesis: verum
end;
hence product ((a,b,c) --> ({x},{y},{z})) = {((a,b,c) --> (x,y,z))} by CARD_3:def_5; ::_thesis: verum
end;
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))
proof
let a, b be set ; ::_thesis: 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))
let c be complex number ; ::_thesis: 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))
let A, B, C, D, E, F be set ; ::_thesis: ( A c= B & C c= D & E c= F implies product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) )
assume A1: ( A c= B & C c= D & E c= F ) ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
set f = (a,b,c) --> (A,C,E);
set g = (a,b,c) --> (B,D,F);
A2: ( dom ((a,b,c) --> (A,C,E)) = {a,b,c} & dom ((a,b,c) --> (B,D,F)) = {a,b,c} ) by BVFUNC14:11;
percases ( ( a = c & a <> b ) or ( b = c & a <> b ) or a = b or ( a <> b & a <> c & b <> c ) ) ;
suppose ( a = c & a <> b ) ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
then ( (a,b,c) --> (A,C,E) = (a,b) --> (E,C) & (a,b,c) --> (B,D,F) = (a,b) --> (F,D) ) by Th25;
hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; ::_thesis: verum
end;
suppose ( b = c & a <> b ) ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
then ( (a,b,c) --> (A,C,E) = (a,b) --> (A,E) & (a,b,c) --> (B,D,F) = (a,b) --> (B,F) ) by Th26;
hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; ::_thesis: verum
end;
suppose a = b ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
then ( (a,b,c) --> (A,C,E) = (a,c) --> (C,E) & (a,b,c) --> (B,D,F) = (a,c) --> (D,F) ) by FUNCT_4:81;
hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; ::_thesis: verum
end;
supposeA3: ( a <> b & a <> c & b <> c ) ; ::_thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
for x being set st x in dom ((a,b,c) --> (A,C,E)) holds
((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x
proof
let x be set ; ::_thesis: ( x in dom ((a,b,c) --> (A,C,E)) implies ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x )
assume x in dom ((a,b,c) --> (A,C,E)) ; ::_thesis: ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x
then A4: ( x = a or x = b or x = c ) by A2, ENUMSET1:def_1;
a,b,c are_mutually_different by A3, ZFMISC_1:def_5;
then ( ((a,b,c) --> (A,C,E)) . a = A & ((a,b,c) --> (A,C,E)) . b = C & ((a,b,c) --> (A,C,E)) . c = E & ((a,b,c) --> (B,D,F)) . a = B & ((a,b,c) --> (B,D,F)) . b = D & ((a,b,c) --> (B,D,F)) . c = F ) by Th28;
hence ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x by A1, A4; ::_thesis: verum
end;
hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A2, CARD_3:27; ::_thesis: verum
end;
end;
end;
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))
proof
let a, b, x, X, y, Y, z, Z be set ; ::_thesis: 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))
let c be complex number ; ::_thesis: ( a,b,c are_mutually_different & x in X & y in Y & z in Z implies (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) )
assume A1: a,b,c are_mutually_different ; ::_thesis: ( not x in X or not y in Y or not z in Z or (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) )
assume ( x in X & y in Y & z in Z ) ; ::_thesis: (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z))
then ( {x} c= X & {y} c= Y & {z} c= Z ) by ZFMISC_1:31;
then product ((a,b,c) --> ({x},{y},{z})) c= product ((a,b,c) --> (X,Y,Z)) by Th32;
then {((a,b,c) --> (x,y,z))} c= product ((a,b,c) --> (X,Y,Z)) by A1, Th31;
hence (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) by ZFMISC_1:31; ::_thesis: verum
end;
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
proof
thus for x, y being complex-valued Function st x in dom {} & - x in dom {} & y = {} . x holds
{} . (- x) = - y ; :: according to BORSUK_7:def_2 ::_thesis: verum
end;
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
proof
take {} ; ::_thesis: {} is odd
thus {} is odd ; ::_thesis: verum
end;
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)*>
proof
let p be Point of (TOP-REAL 3); ::_thesis: sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*>
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3;
hence sqr p = <*((p `1) ^2),((p `2) ^2),((p `3) ^2)*> by Th16; ::_thesis: verum
end;
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)
proof
let p be Point of (TOP-REAL 3); ::_thesis: Sum (sqr p) = (((p `1) ^2) + ((p `2) ^2)) + ((p `3) ^2)
p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3;
hence Sum (sqr p) = (((p `1) ^2) + ((p `2) ^2)) + ((p `3) ^2) by Th17; ::_thesis: verum
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 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)
proof
let r be real number ; ::_thesis: for S being Subset of R^1 st S = RAT holds
RAT /\ ].-infty,r.[ is open Subset of (R^1 | S)
let S be Subset of R^1; ::_thesis: ( S = RAT implies RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) )
assume A1: S = RAT ; ::_thesis: RAT /\ ].-infty,r.[ is open Subset of (R^1 | S)
set X = ].-infty,r.[;
reconsider R = RAT /\ ].-infty,r.[ as Subset of (R^1 | (R^1 QQ)) by Lm8, XBOOLE_1:17;
A2: R^1 ].-infty,r.[ is open by BORSUK_5:40;
R = (R^1 ].-infty,r.[) /\ the carrier of (R^1 | (R^1 QQ)) by PRE_TOPC:8;
hence RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) by A1, A2, TSP_1:def_1; ::_thesis: verum
end;
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)
proof
let r be real number ; ::_thesis: for S being Subset of R^1 st S = RAT holds
RAT /\ ].r,+infty.[ is open Subset of (R^1 | S)
let S be Subset of R^1; ::_thesis: ( S = RAT implies RAT /\ ].r,+infty.[ is open Subset of (R^1 | S) )
assume A1: S = RAT ; ::_thesis: RAT /\ ].r,+infty.[ is open Subset of (R^1 | S)
set X = ].r,+infty.[;
reconsider R = RAT /\ ].r,+infty.[ as Subset of (R^1 | (R^1 QQ)) by Lm8, XBOOLE_1:17;
A2: R^1 ].r,+infty.[ is open by BORSUK_5:40;
R = (R^1 ].r,+infty.[) /\ the carrier of (R^1 | (R^1 QQ)) by PRE_TOPC:8;
hence RAT /\ ].r,+infty.[ is open Subset of (R^1 | S) by A1, A2, TSP_1:def_1; ::_thesis: verum
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_(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 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 (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 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 (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 to XBOOLE_0:def_10 ::_thesis: G1 /\ the carrier of (Image f) c= Q1
proof
let x be set ; :: according to TARSKI: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 to TARSKI: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 to XBOOLE_0:def_10 ::_thesis: G2 /\ the carrier of (Image f) c= Q2
proof
let x be set ; :: according to TARSKI: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 to TARSKI: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 to XBOOLE_0:def_10 ::_thesis: [#] (Image f) c= Q1 \/ Q2
let x be Element of (Image f); :: according to LATTICE7: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
proof
set g = corestr f;
A1: dom (corestr f) = [#] X by FUNCT_2:def_1;
rng (corestr f) = [#] (Image f) by FUNCT_2:def_3;
then (corestr f) .: ([#] X) = [#] (Image f) by A1, RELAT_1:113;
hence Image f is connected by CONNSP_1:14, WAYBEL18:10; ::_thesis: verum
end;
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
proof
let S be Subset of R^1; ::_thesis: ( S = RAT implies for T being connected TopSpace
for f being Function of T,(R^1 | S) st f is continuous holds
f is constant )
assume A1: S = RAT ; ::_thesis: for T being connected TopSpace
for f being Function of T,(R^1 | S) st f is continuous holds
f is constant
let T be connected TopSpace; ::_thesis: for f being Function of T,(R^1 | S) st f is continuous holds
f is constant
let f be Function of T,(R^1 | S); ::_thesis: ( f is continuous implies f is constant )
assume A2: f is continuous ; ::_thesis: f is constant
percases ( not T is empty or T is empty ) ;
supposeA3: not T is empty ; ::_thesis: f is constant
set GX = Image f;
let x, y be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in dom f or not y in dom f or f . x = f . y )
assume that
A4: ( x in dom f & y in dom f ) and
A5: f . x <> f . y ; ::_thesis: contradiction
percases ( f . x < f . y or f . y < f . x ) by A5, XXREAL_0:1;
suppose f . x < f . y ; ::_thesis: contradiction
then 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 ) by A1, A3, A4, Lm9;
hence contradiction by A1, A2, A3, CONNSP_1:11; ::_thesis: verum
end;
suppose f . y < f . x ; ::_thesis: contradiction
then 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 ) by A1, A3, A4, Lm9;
hence contradiction by A1, A2, A3, CONNSP_1:11; ::_thesis: verum
end;
end;
end;
suppose T is empty ; ::_thesis: f is constant
hence f is constant ; ::_thesis: verum
end;
end;
end;
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
proof
set X = R^1 ;
let a, b be real number ; ::_thesis: 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
set S = Closed-Interval-TSpace (a,b);
let f be continuous Function of (Closed-Interval-TSpace (a,b)),R^1; ::_thesis: for g being PartFunc of REAL,REAL st a <= b & f = g holds
g is continuous
let g be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f = g implies g is continuous )
assume that
A1: a <= b and
A2: f = g ; ::_thesis: g is continuous
set A = left_closed_halfline a;
set B = [.a,b.];
set C = right_closed_halfline b;
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18;
then reconsider a1 = a, b1 = b as Point of (Closed-Interval-TSpace (a,b)) by A1, XXREAL_1:1;
set f1 = (R^1 | (R^1 (left_closed_halfline a))) --> (f . a1);
set f2 = (R^1 | (R^1 (right_closed_halfline b))) --> (f . b1);
A3: the carrier of (R^1 | (R^1 (left_closed_halfline a))) = left_closed_halfline a by PRE_TOPC:8;
Closed-Interval-TSpace (a,b) = R^1 | (R^1 [.a,b.]) by A1, TOPMETR:19;
then reconsider f = f as continuous Function of (R^1 | (R^1 [.a,b.])),R^1 ;
A4: dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) = the carrier of (R^1 | (R^1 (left_closed_halfline a))) by FUNCT_2:def_1
.= left_closed_halfline a by PRE_TOPC:8 ;
A5: dom f = the carrier of (R^1 | (R^1 [.a,b.])) by FUNCT_2:def_1
.= [.a,b.] by PRE_TOPC:8 ;
A6: dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) = the carrier of (R^1 | (R^1 (right_closed_halfline b))) by FUNCT_2:def_1
.= right_closed_halfline b by PRE_TOPC:8 ;
b in REAL by XREAL_0:def_1;
then A7: b < +infty by XXREAL_0:9;
(R^1 | (R^1 (left_closed_halfline a))) --> (f . a1) tolerates f
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) /\ (dom f) or ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x )
assume A8: x in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) /\ (dom f) ; ::_thesis: ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x
a in REAL by XREAL_0:def_1;
then (left_closed_halfline a) /\ [.a,b.] = {a} by A1, XXREAL_0:12, XXREAL_1:417;
then A9: x = a by A4, A5, A8, TARSKI:def_1;
then a in left_closed_halfline a by A4, A8, XBOOLE_0:def_4;
hence ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x = f . x by A3, A9, FUNCOP_1:7; ::_thesis: verum
end;
then reconsider ff = ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) +* f as continuous Function of (R^1 | ((R^1 (left_closed_halfline a)) \/ (R^1 [.a,b.]))),R^1 by TOPGEN_5:10;
set G = ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1));
ff tolerates (R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom ff) /\ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) or ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x )
assume A10: x in (dom ff) /\ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) ; ::_thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x
then A11: x in dom ff by XBOOLE_0:def_4;
A12: x in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A10, XBOOLE_0:def_4;
then reconsider y = x as Real by A6;
A13: b <= y by A6, A12, XXREAL_1:3;
A14: dom ff = (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f) by FUNCT_4:def_1;
percases ( ( x in dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) & not x in dom f ) or x in dom f ) by A11, A14, XBOOLE_0:def_3;
supposethat A15: x in dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) and
A16: not x in dom f ; ::_thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x
y <= a by A4, A15, XXREAL_1:2;
then b <= a by A13, XXREAL_0:2;
then a = b by A1, XXREAL_0:1;
hence ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x = f . a1 by A10, FUNCOP_1:7
.= ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1)) . x by A15, FUNCOP_1:7
.= ff . x by A16, FUNCT_4:11 ;
::_thesis: verum
end;
supposeA17: x in dom f ; ::_thesis: ff . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x
then y <= b by A5, XXREAL_1:1;
then b = y by A13, XXREAL_0:1;
hence ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x = f . x by A10, FUNCOP_1:7
.= ff . x by A17, FUNCT_4:13 ;
::_thesis: verum
end;
end;
end;
then A18: ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) is continuous Function of (R^1 | ((R^1 ((left_closed_halfline a) \/ [.a,b.])) \/ (R^1 (right_closed_halfline b)))),R^1 by TOPGEN_5:10;
A19: ((left_closed_halfline a) \/ [.a,b.]) \/ (right_closed_halfline b) c= REAL ;
A20: dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) = (dom ff) \/ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by FUNCT_4:def_1
.= ((dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f)) \/ (dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by FUNCT_4:def_1 ;
A21: dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) = REAL
proof
thus dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) c= REAL by A4, A5, A6, A19, A20; :: according to XBOOLE_0:def_10 ::_thesis: REAL c= dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL or x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) )
assume x in REAL ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
then reconsider y = x as Real ;
A22: y < +infty by XXREAL_0:9;
A23: -infty < y by XXREAL_0:12;
percases ( y < b or y >= b ) ;
supposeA24: y < b ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
percases ( y < a or y >= a ) ;
suppose y < a ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
then y in left_closed_halfline a by A23, XXREAL_1:2;
then y in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f) by A4, XBOOLE_0:def_3;
hence x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by A20, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose y >= a ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
then y in [.a,b.] by A24, XXREAL_1:1;
then y in (dom ((R^1 | (R^1 (left_closed_halfline a))) --> (f . a1))) \/ (dom f) by A5, XBOOLE_0:def_3;
hence x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by A20, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
suppose y >= b ; ::_thesis: x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)))
then y in right_closed_halfline b by A22, XXREAL_1:3;
hence x in dom (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) by A6, A20, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then ((left_closed_halfline a) \/ [.a,b.]) \/ (right_closed_halfline b) = [#] R^1 by A4, A5, A6, A20, TOPMETR:17;
then A25: R^1 | ((R^1 ((left_closed_halfline a) \/ [.a,b.])) \/ (R^1 (right_closed_halfline b))) = R^1 by TSEP_1:3;
rng (ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1))) c= REAL by TOPMETR:17;
then reconsider G = ff +* ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) as PartFunc of REAL,REAL by A21, RELSET_1:4;
A26: G is continuous by A18, A25, JORDAN5A:7;
A27: dom f = (dom G) /\ [.a,b.] by A5, A21, XBOOLE_1:28;
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
G_._x_=_f_._x
let x be set ; ::_thesis: ( x in dom f implies G . b1 = f . b1 )
assume A28: x in dom f ; ::_thesis: G . b1 = f . b1
then reconsider y = x as Real by A5;
A29: y <= b by A5, A28, XXREAL_1:1;
percases ( y < b or y = b ) by A29, XXREAL_0:1;
suppose y < b ; ::_thesis: G . b1 = f . b1
then not y in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A6, XXREAL_1:3;
hence G . x = ff . x by FUNCT_4:11
.= f . x by A28, FUNCT_4:13 ;
::_thesis: verum
end;
supposeA30: y = b ; ::_thesis: G . b1 = f . b1
then A31: x in dom ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) by A6, A7, XXREAL_1:3;
hence G . x = ((R^1 | (R^1 (right_closed_halfline b))) --> (f . b1)) . x by FUNCT_4:13
.= f . x by A30, A31, FUNCOP_1:7 ;
::_thesis: verum
end;
end;
end;
then g = G | [.a,b.] by A2, A27, FUNCT_1:46;
hence g is continuous by A26; ::_thesis: verum
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 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
proof
r + f is Function of X,REAL ;
hence r + f is Function of X,R^1 by TOPMETR:17; ::_thesis: verum
end;
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
proof
f - r is Function of X,REAL ;
hence f - r is Function of X,R^1 by TOPMETR:17; ::_thesis: verum
end;
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
proof
now__::_thesis:_(_f_+_r_is_continuous_&_(f_+_r)_._0_=_s_+_r_&_(f_+_r)_._1_=_t_+_r_)
thus f + r is continuous ; ::_thesis: ( (f + r) . 0 = s + r & (f + r) . 1 = t + r )
thus (f + r) . 0 = (f . j0) + r by VALUED_1:2
.= s + r by BORSUK_2:def_4 ; ::_thesis: (f + r) . 1 = t + r
thus (f + r) . 1 = (f . j1) + r by VALUED_1:2
.= t + r by BORSUK_2:def_4 ; ::_thesis: verum
end;
hence r + f is Path of s + r,t + r by BORSUK_2:def_4; ::_thesis: verum
end;
:: original: -
redefine funcf - r -> Path of s - r,t - r;
coherence
f - r is Path of s - r,t - r
proof
now__::_thesis:_(_f_-_r_is_continuous_&_(f_-_r)_._0_=_s_-_r_&_(f_-_r)_._1_=_t_-_r_)
thus f - r is continuous ; ::_thesis: ( (f - r) . 0 = s - r & (f - r) . 1 = t - r )
thus (f - r) . 0 = (f . j0) - r by VALUED_1:2
.= s - r by BORSUK_2:def_4 ; ::_thesis: (f - r) . 1 = t - r
thus (f - r) . 1 = (f . j1) - r by VALUED_1:2
.= t - r by BORSUK_2:def_4 ; ::_thesis: verum
end;
hence f - r is Path of s - r,t - r by BORSUK_2:def_4; ::_thesis: verum
end;
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)
proof
set p = |[1,0,0]|;
|.(|[1,0,0]| - (0. (TOP-REAL 3))).| = |.|[1,0,0]|.| by RLVECT_1:13
.= sqrt ((((|[1,0,0]| `1) ^2) + ((|[1,0,0]| `2) ^2)) + ((|[1,0,0]| `3) ^2)) by Th35
.= sqrt (((1 ^2) + ((|[1,0,0]| `2) ^2)) + ((|[1,0,0]| `3) ^2)) by EUCLID_5:2
.= sqrt (((1 ^2) + (Q ^2)) + ((|[1,0,0]| `3) ^2)) by EUCLID_5:2
.= 1 by EUCLID_5:2, SQUARE_1:18 ;
then |[1,0,0]| in Sphere ((0. (TOP-REAL 3)),1) by TOPREAL9:9;
hence |[1,0,0]| is Point of (Tunit_circle 3) by TOPREALB:9; ::_thesis: verum
end;
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)
proof
|[(- 1),(- Q),(- Q)]| = - c100 by EUCLID_5:11
.= - c[100] ;
hence |[(- 1),0,0]| is Point of (Tunit_circle 3) by TOPREALC:60; ::_thesis: verum
end;
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]
proof
- c100 = |[(- 1),(- Q),(- Q)]| by EUCLID_5:11
.= c[-100] ;
hence - c[100] = c[-100] ; ::_thesis: verum
end;
theorem :: BORSUK_7:41
- c[-100] = c[100] by Th40;
theorem :: BORSUK_7:42
c[100] - c[-100] = |[2,0,0]|
proof
c100 - mc100 = |[(1 - (- 1)),(Q - Q),(Q - Q)]| by EUCLID_5:13
.= |[2,0,0]| ;
hence c[100] - c[-100] = |[2,0,0]| ; ::_thesis: verum
end;
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)) )
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) )
set c = euc2cpx p;
A1: euc2cpx p = (|.(euc2cpx p).| * (cos (Arg (euc2cpx p)))) + ((|.(euc2cpx p).| * (sin (Arg (euc2cpx p)))) * **) by COMPTRIG:62;
A2: |.(euc2cpx p).| = |.p.| by EUCLID_3:25;
( Re (euc2cpx p) = p `1 & Im (euc2cpx p) = p `2 ) by COMPLEX1:12;
hence ( p `1 = |.p.| * (cos (Arg p)) & p `2 = |.p.| * (sin (Arg p)) ) by A1, A2, COMPLEX1:12; ::_thesis: verum
end;
theorem :: BORSUK_7:44
for p being Point of (TOP-REAL 2) holds p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * **))
proof
let p be Point of (TOP-REAL 2); ::_thesis: p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * **))
set c = euc2cpx p;
A1: euc2cpx p = (|.(euc2cpx p).| * (cos (Arg (euc2cpx p)))) + ((|.(euc2cpx p).| * (sin (Arg (euc2cpx p)))) * **) by COMPTRIG:62;
|.(euc2cpx p).| = |.p.| by EUCLID_3:25;
hence p = cpx2euc ((|.p.| * (cos (Arg p))) + ((|.p.| * (sin (Arg p))) * **)) by A1, EUCLID_3:2; ::_thesis: verum
end;
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
proof
let i be Integer; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) holds
p1 = p2
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) implies p1 = p2 )
( |.(euc2cpx p1).| = |.p1.| & |.(euc2cpx p2).| = |.p2.| ) by EUCLID_3:25;
hence ( |.p1.| = |.p2.| & Arg p1 = (Arg p2) + ((2 * PI) * i) implies p1 = p2 ) by Th12, EUCLID_3:4; ::_thesis: verum
end;
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)
proof
let r be real number ; ::_thesis: for p being Point of (TOP-REAL 2) st p = CircleMap . r holds
Arg p = (2 * PI) * (frac r)
let p be Point of (TOP-REAL 2); ::_thesis: ( p = CircleMap . r implies Arg p = (2 * PI) * (frac r) )
set z = euc2cpx p;
set A = (2 * PI) * (frac r);
assume A1: p = CircleMap . r ; ::_thesis: Arg p = (2 * PI) * (frac r)
reconsider q = CircleMap . (R^1 r) as Point of (TOP-REAL 2) by PRE_TOPC:25;
A2: |.(euc2cpx p).| = |.p.| by EUCLID_3:25;
A3: |.q.| = 1 by TOPREALB:12;
( frac r < 1 & 0 <= frac r ) by INT_1:43;
then A4: ( (2 * PI) * Q <= (2 * PI) * (frac r) & (2 * PI) * (frac r) < (2 * PI) * 1 ) by XREAL_1:68;
A5: ( |[(cos ((2 * PI) * r)),(sin ((2 * PI) * r))]| `1 = cos ((2 * PI) * r) & |[(cos ((2 * PI) * r)),(sin ((2 * PI) * r))]| `2 = sin ((2 * PI) * r) ) by EUCLID:52;
A6: CircleMap . r = |[(cos ((2 * PI) * r)),(sin ((2 * PI) * r))]| by TOPREALB:def_11;
(2 * PI) * (frac r) = ((2 * PI) * r) + ((2 * PI) * (- [\r/])) ;
then ( cos ((2 * PI) * r) = cos ((2 * PI) * (frac r)) & sin ((2 * PI) * r) = sin ((2 * PI) * (frac r)) ) by COMPLEX2:8, COMPLEX2:9;
then euc2cpx p = (|.(euc2cpx p).| * (cos ((2 * PI) * (frac r)))) + ((|.(euc2cpx p).| * (sin ((2 * PI) * (frac r)))) * **) by A1, A2, A3, A5, A6;
hence Arg p = (2 * PI) * (frac r) by A4, A2, A1, A3, COMPLEX1:44, COMPTRIG:def_1; ::_thesis: verum
end;
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))
proof
let p1, p2 be Point of (TOP-REAL 3); ::_thesis: 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))
let u1, u2 be Point of (Euclid 3); ::_thesis: ( u1 = p1 & u2 = p2 implies (Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2)) )
assume A1: ( u1 = p1 & u2 = p2 ) ; ::_thesis: (Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2))
A2: p1 = |[(p1 `1),(p1 `2),(p1 `3)]| by EUCLID_5:3;
A3: u2 = <*(p2 `1),(p2 `2),(p2 `3)*> by A1, EUCLID_5:3;
reconsider v1 = u1, v2 = u2 as Element of REAL 3 ;
v1 - v2 = <*(diffreal . ((p1 `1),(p2 `1))),(diffreal . ((p1 `2),(p2 `2))),(diffreal . ((p1 `3),(p2 `3)))*> by A1, A2, A3, FINSEQ_2:76
.= <*((p1 `1) - (p2 `1)),(diffreal . ((p1 `2),(p2 `2))),(diffreal . ((p1 `3),(p2 `3)))*> by BINOP_2:def_10
.= <*((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2)),(diffreal . ((p1 `3),(p2 `3)))*> by BINOP_2:def_10
.= <*((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2)),((p1 `3) - (p2 `3))*> by BINOP_2:def_10 ;
then abs (v1 - v2) = <*(absreal . ((p1 `1) - (p2 `1))),(absreal . ((p1 `2) - (p2 `2))),(absreal . ((p1 `3) - (p2 `3)))*> by FINSEQ_2:37
.= <*(abs ((p1 `1) - (p2 `1))),(absreal . ((p1 `2) - (p2 `2))),(absreal . ((p1 `3) - (p2 `3)))*> by EUCLID:def_2
.= <*(abs ((p1 `1) - (p2 `1))),(abs ((p1 `2) - (p2 `2))),(absreal . ((p1 `3) - (p2 `3)))*> by EUCLID:def_2
.= <*(abs ((p1 `1) - (p2 `1))),(abs ((p1 `2) - (p2 `2))),(abs ((p1 `3) - (p2 `3)))*> by EUCLID:def_2 ;
then A4: sqr (abs (v1 - v2)) = <*(sqrreal . (abs ((p1 `1) - (p2 `1)))),(sqrreal . (abs ((p1 `2) - (p2 `2)))),(sqrreal . (abs ((p1 `3) - (p2 `3))))*> by FINSEQ_2:37
.= <*((abs ((p1 `1) - (p2 `1))) ^2),(sqrreal . (abs ((p1 `2) - (p2 `2)))),(sqrreal . (abs ((p1 `3) - (p2 `3))))*> by RVSUM_1:def_2
.= <*((abs ((p1 `1) - (p2 `1))) ^2),((abs ((p1 `2) - (p2 `2))) ^2),(sqrreal . (abs ((p1 `3) - (p2 `3))))*> by RVSUM_1:def_2
.= <*((abs ((p1 `1) - (p2 `1))) ^2),((abs ((p1 `2) - (p2 `2))) ^2),((abs ((p1 `3) - (p2 `3))) ^2)*> by RVSUM_1:def_2
.= <*(((p1 `1) - (p2 `1)) ^2),((abs ((p1 `2) - (p2 `2))) ^2),((abs ((p1 `3) - (p2 `3))) ^2)*> by COMPLEX1:75
.= <*(((p1 `1) - (p2 `1)) ^2),(((p1 `2) - (p2 `2)) ^2),((abs ((p1 `3) - (p2 `3))) ^2)*> by COMPLEX1:75
.= <*(((p1 `1) - (p2 `1)) ^2),(((p1 `2) - (p2 `2)) ^2),(((p1 `3) - (p2 `3)) ^2)*> by COMPLEX1:75 ;
(Pitag_dist 3) . (u1,u2) = |.(v1 - v2).| by EUCLID:def_6
.= sqrt (Sum (sqr (abs (v1 - v2)))) by EUCLID:25 ;
hence (Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2)) by A4, RVSUM_1:78; ::_thesis: verum
end;
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)
proof
let r be real number ; ::_thesis: 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)
let p be Point of (TOP-REAL 3); ::_thesis: 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)
let e be Point of (Euclid 3); ::_thesis: ( p = e & p `3 = 0 implies 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) )
set A = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[;
set B = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[;
set C = {0};
set f = (1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0});
assume that
A1: p = e and
A2: p `3 = 0 ; ::_thesis: 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)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in 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})) or a in Ball (e,r) )
assume a in 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})) ; ::_thesis: a in Ball (e,r)
then consider g being Function such that
A3: a = g and
A4: dom g = dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) and
A5: for x being set st x in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) holds
g . x in ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . x by CARD_3:def_5;
A6: ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ = { m where m is Real : ( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) ) } by RCOMP_1:def_2;
A7: ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ = { n where n is Real : ( (p `2) - (r / (sqrt 2)) < n & n < (p `2) + (r / (sqrt 2)) ) } by RCOMP_1:def_2;
A8: dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) = {1,2,3} by BVFUNC14:11;
then A9: ( 1 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) & 2 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) & 3 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) ) by ENUMSET1:def_1;
A10: ( ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 1 = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ & ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 2 = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ & ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 3 = {0} ) by Lm6, Th28;
then A11: ( g . 1 in ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ & g . 2 in ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ & g . 3 in {0} ) by A5, A9;
then consider m being Real such that
A12: m = g . 1 and
( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) ) by A6;
consider n being Real such that
A13: n = g . 2 and
( (p `2) - (r / (sqrt 2)) < n & n < (p `2) + (r / (sqrt 2)) ) by A7, A11;
g . 3 in ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 3 by A5, A9;
then A14: g . 3 = 0 by A10, TARSKI:def_1;
(p `1) + (r / (sqrt 2)) > (p `1) - (r / (sqrt 2)) by A11, XXREAL_1:28;
then (p `1) - ((p `1) + (r / (sqrt 2))) < (p `1) - ((p `1) - (r / (sqrt 2))) by XREAL_1:10;
then (- (r / (sqrt 2))) + (r / (sqrt 2)) < (r / (sqrt 2)) + (r / (sqrt 2)) by XREAL_1:6;
then A15: 0 < r ;
A16: dom <*(g . 1),(g . 2),(g . 3)*> = Seg (len <*(g . 1),(g . 2),(g . 3)*>) by FINSEQ_1:def_3
.= {1,2,3} by FINSEQ_3:1, FINSEQ_1:45 ;
now__::_thesis:_for_k_being_set_st_k_in_dom_g_holds_
g_._k_=_<*(g_._1),(g_._2),(g_._3)*>_._k
let k be set ; ::_thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2),(g . 3)*> . k )
assume k in dom g ; ::_thesis: g . k = <*(g . 1),(g . 2),(g . 3)*> . k
then ( k = 1 or k = 2 or k = 3 ) by A4, A8, ENUMSET1:def_1;
hence g . k = <*(g . 1),(g . 2),(g . 3)*> . k by FINSEQ_1:45; ::_thesis: verum
end;
then A17: a = |[m,n,0]| by A3, A4, A12, A13, A16, A14, BVFUNC14:11, FUNCT_1:2;
then reconsider c = a as Point of (TOP-REAL 3) ;
reconsider b = c as Point of (Euclid 3) by TOPREAL3:8;
( abs (m - (p `1)) < r / (sqrt 2) & abs (n - (p `2)) < r / (sqrt 2) ) by A11, A12, A13, RCOMP_1:1;
then ( (abs (m - (p `1))) ^2 < (r / (sqrt 2)) ^2 & (abs (n - (p `2))) ^2 < (r / (sqrt 2)) ^2 ) by SQUARE_1:16;
then ( (abs (m - (p `1))) ^2 < (r ^2) / ((sqrt 2) ^2) & (abs (n - (p `2))) ^2 < (r ^2) / ((sqrt 2) ^2) ) by XCMPLX_1:76;
then ( (abs (m - (p `1))) ^2 < (r ^2) / 2 & (abs (n - (p `2))) ^2 < (r ^2) / 2 ) by SQUARE_1:def_2;
then ( (m - (p `1)) ^2 < (r ^2) / 2 & (n - (p `2)) ^2 < (r ^2) / 2 ) by COMPLEX1:75;
then ((m - (p `1)) ^2) + ((n - (p `2)) ^2) < ((r ^2) / 2) + ((r ^2) / 2) by XREAL_1:8;
then sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < sqrt (r ^2) by SQUARE_1:27;
then A18: sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < r by A15, SQUARE_1:22;
A19: ( m = c `1 & n = c `2 ) by A17, EUCLID_5:2;
dist (b,e) = (Pitag_dist 3) . (b,e) by METRIC_1:def_1
.= sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + (((c `3) - (p `3)) ^2)) by A1, Th47
.= sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + ((Q - Q) ^2)) by A2, A17, EUCLID_5:2
.= sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + Q) ;
hence a in Ball (e,r) by A18, A19, METRIC_1:11; ::_thesis: verum
end;
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)))
proof
let i be Integer; ::_thesis: for c being complex number
for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))
let c be complex number ; ::_thesis: for s being Real holds Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))
let s be Real; ::_thesis: Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i)))
( cos (s + (Arg c)) = cos ((s + (Arg c)) + ((2 * PI) * i)) & sin (s + (Arg c)) = sin ((s + (Arg c)) + ((2 * PI) * i)) ) by COMPLEX2:8, COMPLEX2:9;
hence Rotate (c,s) = Rotate (c,(s + ((2 * PI) * i))) ; ::_thesis: verum
end;
theorem :: BORSUK_7:50
for i being Integer
for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i))
proof
let i be Integer; ::_thesis: for s being Real holds Rotate s = Rotate (s + ((2 * PI) * i))
let s be Real; ::_thesis: Rotate s = Rotate (s + ((2 * PI) * i))
let p be Point of (TOP-REAL 2); :: according to FUNCT_2:def_8 ::_thesis: (Rotate s) . p = (Rotate (s + ((2 * PI) * i))) . p
set q = (p `1) + ((p `2) * **);
A1: Rotate (((p `1) + ((p `2) * **)),s) = Rotate (((p `1) + ((p `2) * **)),(s + ((2 * PI) * i))) by Th49;
thus (Rotate s) . p = |[(Re (Rotate (((p `1) + ((p `2) * **)),s))),(Im (Rotate (((p `1) + ((p `2) * **)),s)))]| by JORDAN24:def_3
.= (Rotate (s + ((2 * PI) * i))) . p by A1, JORDAN24:def_3 ; ::_thesis: verum
end;
theorem Th51: :: BORSUK_7:51
for s being Real
for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.|
proof
let s be Real; ::_thesis: for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.|
let p be Point of (TOP-REAL 2); ::_thesis: |.((Rotate s) . p).| = |.p.|
set c = euc2cpx p;
set q = (Rotate s) . p;
A1: ( Re (Rotate ((euc2cpx p),s)) = |.(euc2cpx p).| * (cos (s + (Arg (euc2cpx p)))) & Im (Rotate ((euc2cpx p),s)) = |.(euc2cpx p).| * (sin (s + (Arg (euc2cpx p)))) ) by COMPLEX1:12;
(Rotate s) . p = cpx2euc (Rotate ((euc2cpx p),s)) by JORDAN24:def_3;
then A2: ( ((Rotate s) . p) `1 = Re (Rotate ((euc2cpx p),s)) & ((Rotate s) . p) `2 = Im (Rotate ((euc2cpx p),s)) ) by EUCLID:52;
|.p.| ^2 = (|.(euc2cpx p).| ^2) * 1 by EUCLID_3:25
.= (|.(euc2cpx p).| ^2) * (((cos (s + (Arg (euc2cpx p)))) ^2) + ((sin (s + (Arg (euc2cpx p)))) ^2)) by SIN_COS:29
.= ((|.(euc2cpx p).| * (cos (s + (Arg (euc2cpx p))))) ^2) + ((|.(euc2cpx p).| * (sin (s + (Arg (euc2cpx p))))) ^2)
.= |.((Rotate s) . p).| ^2 by A1, A2, JGRAPH_1:29 ;
hence |.p.| = |.((Rotate s) . p).| by Th1; ::_thesis: verum
end;
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))
proof
let s be Real; ::_thesis: for p being Point of (TOP-REAL 2) holds Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s))
let p be Point of (TOP-REAL 2); ::_thesis: Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s))
(Rotate s) . p = cpx2euc (Rotate ((euc2cpx p),s)) by JORDAN24:def_3;
hence Arg ((Rotate s) . p) = Arg (Rotate ((euc2cpx p),s)) by EUCLID_3:1; ::_thesis: verum
end;
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)
proof
let s be Real; ::_thesis: 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)
let p be Point of (TOP-REAL 2); ::_thesis: ( p <> 0. (TOP-REAL 2) implies ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i) )
set c = euc2cpx p;
assume p <> 0. (TOP-REAL 2) ; ::_thesis: ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i)
then ex i being Integer st Arg (Rotate ((euc2cpx p),s)) = ((2 * PI) * i) + (s + (Arg (euc2cpx p))) by COMPLEX2:54, EUCLID_3:18;
hence ex i being Integer st Arg ((Rotate s) . p) = (s + (Arg p)) + ((2 * PI) * i) by Th52; ::_thesis: verum
end;
theorem Th54: :: BORSUK_7:54
for s being Real holds (Rotate s) . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)
proof
let s be Real; ::_thesis: (Rotate s) . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)
thus (Rotate s) . (0. (TOP-REAL 2)) = cpx2euc (Rotate ((euc2cpx (0. (TOP-REAL 2))),s)) by JORDAN24:def_3
.= 0. (TOP-REAL 2) by COMPLEX2:52, EUCLID_3:16, EUCLID_3:17 ; ::_thesis: verum
end;
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)
proof
let s be Real; ::_thesis: for p being Point of (TOP-REAL 2) st (Rotate s) . p = 0. (TOP-REAL 2) holds
p = 0. (TOP-REAL 2)
let p be Point of (TOP-REAL 2); ::_thesis: ( (Rotate s) . p = 0. (TOP-REAL 2) implies p = 0. (TOP-REAL 2) )
|.p.| = |.((Rotate s) . p).| by Th51;
hence ( (Rotate s) . p = 0. (TOP-REAL 2) implies p = 0. (TOP-REAL 2) ) by TOPRNS_1:23, TOPRNS_1:24; ::_thesis: verum
end;
theorem Th56: :: BORSUK_7:56
for s being Real
for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p
proof
let s be Real; ::_thesis: for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p
let p be Point of (TOP-REAL 2); ::_thesis: (Rotate s) . ((Rotate (- s)) . p) = p
set f = Rotate s;
set g = Rotate (- s);
percases ( p <> 0. (TOP-REAL 2) or p = 0. (TOP-REAL 2) ) ;
supposeA1: p <> 0. (TOP-REAL 2) ; ::_thesis: (Rotate s) . ((Rotate (- s)) . p) = p
then consider i being Integer such that
A2: Arg ((Rotate (- s)) . p) = ((- s) + (Arg p)) + ((2 * PI) * i) by Th53;
consider j being Integer such that
A3: Arg ((Rotate s) . ((Rotate (- s)) . p)) = (s + (Arg ((Rotate (- s)) . p))) + ((2 * PI) * j) by A1, Th55, Th53;
A4: |.((Rotate s) . ((Rotate (- s)) . p)).| = |.((Rotate (- s)) . p).| by Th51
.= |.p.| by Th51 ;
Arg ((Rotate s) . ((Rotate (- s)) . p)) = (Arg p) + ((2 * PI) * (i + j)) by A2, A3;
hence (Rotate s) . ((Rotate (- s)) . p) = p by A4, Th45; ::_thesis: verum
end;
supposeA5: p = 0. (TOP-REAL 2) ; ::_thesis: (Rotate s) . ((Rotate (- s)) . p) = p
(Rotate s) . ((Rotate (- s)) . (0. (TOP-REAL 2))) = (Rotate s) . (0. (TOP-REAL 2)) by Th54
.= 0. (TOP-REAL 2) by Th54 ;
hence (Rotate s) . ((Rotate (- s)) . p) = p by A5; ::_thesis: verum
end;
end;
end;
theorem :: BORSUK_7:57
for s being Real holds (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2)
proof
let s be Real; ::_thesis: (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2)
let p be Point of (TOP-REAL 2); :: according to FUNCT_2:def_8 ::_thesis: ((Rotate s) * (Rotate (- s))) . p = (id (TOP-REAL 2)) . p
set f = Rotate s;
set g = Rotate (- s);
thus ((Rotate s) * (Rotate (- s))) . p = (Rotate s) . ((Rotate (- s)) . p) by FUNCT_2:15
.= p by Th56
.= (id (TOP-REAL 2)) . p by FUNCT_1:18 ; ::_thesis: verum
end;
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) )
proof
let r be real number ; ::_thesis: 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) )
let s be Real; ::_thesis: 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) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in Sphere ((0. (TOP-REAL 2)),r) iff (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) )
A1: |.p.| = |.((Rotate s) . p).| by Th51;
A2: ((Rotate s) . p) - (0. (TOP-REAL 2)) = (Rotate s) . p by RLVECT_1:13;
hereby ::_thesis: ( (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) implies p in Sphere ((0. (TOP-REAL 2)),r) )
assume p in Sphere ((0. (TOP-REAL 2)),r) ; ::_thesis: (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r)
then |.p.| = r by TOPREAL9:12;
hence (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) by A1, A2, TOPREAL9:9; ::_thesis: verum
end;
assume (Rotate s) . p in Sphere ((0. (TOP-REAL 2)),r) ; ::_thesis: p in Sphere ((0. (TOP-REAL 2)),r)
then A3: |.((Rotate s) . p).| = r by TOPREAL9:12;
A4: (Rotate (- s)) . ((Rotate (- (- s))) . p) = p by Th56;
((Rotate (- s)) . ((Rotate s) . p)) - (0. (TOP-REAL 2)) = (Rotate (- s)) . ((Rotate s) . p) by RLVECT_1:13;
hence p in Sphere ((0. (TOP-REAL 2)),r) by A4, A3, A1, TOPREAL9:9; ::_thesis: verum
end;
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)
proof
let r be real non negative number ; ::_thesis: for s being Real holds (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r)
let s be Real; ::_thesis: (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r)
set f = Rotate s;
set C = Sphere ((0. (TOP-REAL 2)),r);
thus (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) c= Sphere ((0. (TOP-REAL 2)),r) :: according to XBOOLE_0:def_10 ::_thesis: Sphere ((0. (TOP-REAL 2)),r) c= (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r))
proof
let y be Point of (TOP-REAL 2); :: according to LATTICE7:def_1 ::_thesis: ( not y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) or y in Sphere ((0. (TOP-REAL 2)),r) )
assume y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) ; ::_thesis: y in Sphere ((0. (TOP-REAL 2)),r)
then ex c being Element of (TOP-REAL 2) st
( c in Sphere ((0. (TOP-REAL 2)),r) & y = (Rotate s) . c ) by FUNCT_2:65;
hence y in Sphere ((0. (TOP-REAL 2)),r) by Th58; ::_thesis: verum
end;
let y be Point of (TOP-REAL 2); :: according to LATTICE7:def_1 ::_thesis: ( not y in Sphere ((0. (TOP-REAL 2)),r) or y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) )
set x = (Rotate (- s)) . y;
assume y in Sphere ((0. (TOP-REAL 2)),r) ; ::_thesis: y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r))
then (Rotate (- s)) . y in Sphere ((0. (TOP-REAL 2)),r) by Th58;
then (Rotate s) . ((Rotate (- s)) . y) in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) by FUNCT_2:35;
hence y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) by Th56; ::_thesis: verum
end;
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))
proof
set T = Tcircle ((0. (TOP-REAL 2)),r);
set f = (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r));
set C = the carrier of (Tcircle ((0. (TOP-REAL 2)),r));
A1: dom ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) = the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) by FUNCT_2:def_1;
for x being set st x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) holds
((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r))
proof
let x be set ; ::_thesis: ( x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) implies ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) )
assume A2: x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) ; ::_thesis: ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r))
then A3: ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x = (Rotate s) . x by FUNCT_1:49;
the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) by TOPREALB:9;
hence ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) by A3, A2, Th58; ::_thesis: verum
end;
hence (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)) is Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r)) by A1, FUNCT_2:3; ::_thesis: verum
end;
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
proof
set T = Tcircle ((0. (TOP-REAL 2)),r);
set C = [#] (Tcircle ((0. (TOP-REAL 2)),r));
[#] (Tcircle ((0. (TOP-REAL 2)),r)) c= [#] (TOP-REAL 2) by PRE_TOPC:def_4;
then reconsider C = [#] (Tcircle ((0. (TOP-REAL 2)),r)) as Subset of (TOP-REAL 2) ;
A1: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8;
then reconsider f = Rotate s as Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) ;
A2: ( f is onto & f is isometric ) by JORDAN24:2;
reconsider A = C as Subset of (TopSpaceMetr (Euclid 2)) by A1;
(TOP-REAL 2) | C = Tcircle ((0. (TOP-REAL 2)),r) by PRE_TOPC:def_5;
then A3: (TopSpaceMetr (Euclid 2)) | A = Tcircle ((0. (TOP-REAL 2)),r) by A1, PRE_TOPC:36;
the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) by TOPREALB:9;
then (Rotate s) .: C = C by Th59;
hence RotateCircle (r,s) is being_homeomorphism by A2, A3, JORDAN24:14; ::_thesis: verum
end;
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)
proof
let r2, r1 be real number ; ::_thesis: for p being Point of (TOP-REAL 2) st p = CircleMap . r2 holds
(RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2)
let p be Point of (TOP-REAL 2); ::_thesis: ( p = CircleMap . r2 implies (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2) )
assume A1: p = CircleMap . r2 ; ::_thesis: (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = CircleMap . (r1 - r2)
set s = - (Arg p);
reconsider q = CircleMap . (R^1 r1), w = CircleMap . (R^1 (r1 - r2)) as Point of (TOP-REAL 2) by PRE_TOPC:25;
|.q.| = 1 by TOPREALB:12;
then q <> 0. (TOP-REAL 2) by TOPRNS_1:23;
then consider i being Integer such that
A2: Arg ((Rotate (- (Arg p))) . q) = ((- (Arg p)) + (Arg q)) + ((2 * PI) * i) by Th53;
A3: Arg p = (2 * PI) * (frac r2) by A1, Th46;
A4: |.((Rotate (- (Arg p))) . q).| = |.q.| by Th51
.= 1 by TOPREALB:12
.= |.w.| by TOPREALB:12 ;
consider j being Integer such that
A5: frac (r1 - r2) = ((frac r1) - (frac r2)) + j and
( j = 0 or j = 1 ) by Th4;
A6: Arg ((Rotate (- (Arg p))) . q) = ((- ((2 * PI) * (frac r2))) + ((2 * PI) * (frac r1))) + ((2 * PI) * i) by A2, A3, Th46
.= ((2 * PI) * (frac (r1 - r2))) + ((2 * PI) * (i - j)) by A5
.= (Arg w) + ((2 * PI) * (i - j)) by Th46 ;
thus (RotateCircle (1,(- (Arg p)))) . (CircleMap . r1) = (Rotate (- (Arg p))) . q by FUNCT_1:49
.= CircleMap . (r1 - r2) by A4, A6, Th45 ; ::_thesis: verum
end;
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
proof
set U = Tunit_circle n;
set C = Tcircle (p,r);
defpred S1[ Point of (Tunit_circle n), set ] means ex w being Point of (TOP-REAL n) st
( w = $1 & $2 = (r * w) + p );
A1: r is Real by XREAL_0:def_1;
A2: n in NAT by ORDINAL1:def_12;
then A3: the carrier of (Tcircle (p,r)) = Sphere (p,r) by TOPREALB:9;
A4: for u being Point of (Tunit_circle n) ex y being Point of (Tcircle (p,r)) st S1[u,y]
proof
let u be Point of (Tunit_circle n); ::_thesis: ex y being Point of (Tcircle (p,r)) st S1[u,y]
reconsider v = u as Point of (TOP-REAL n) by PRE_TOPC:25;
set y = (r * v) + p;
|.(((r * v) + p) - p).| = |.(r * v).| by EUCLID:48
.= (abs r) * |.v.| by A2, A1, TOPRNS_1:7
.= r * |.v.| by ABSVALUE:def_1
.= r * 1 by A2, TOPREALB:12 ;
then reconsider y = (r * v) + p as Point of (Tcircle (p,r)) by A2, A3, TOPREAL9:9;
take y ; ::_thesis: S1[u,y]
thus S1[u,y] ; ::_thesis: verum
end;
consider f being Function of (Tunit_circle n),(Tcircle (p,r)) such that
A5: for x being Point of (Tunit_circle n) holds S1[x,f . x] from FUNCT_2:sch_3(A4);
take f ; ::_thesis: for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p
let a be Point of (Tunit_circle n); ::_thesis: for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p
let b be Point of (TOP-REAL n); ::_thesis: ( a = b implies f . a = (r * b) + p )
S1[a,f . a] by A5;
hence ( a = b implies f . a = (r * b) + p ) ; ::_thesis: verum
end;
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
proof
let f, g be Function of (Tunit_circle n),(Tcircle (p,r)); ::_thesis: ( ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) & ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
g . a = (r * b) + p ) implies f = g )
assume that
A6: for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p and
A7: for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
g . a = (r * b) + p ; ::_thesis: f = g
let x be Point of (Tunit_circle n); :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x
reconsider y = x as Point of (TOP-REAL n) by PRE_TOPC:25;
thus f . x = (r * y) + p by A6
.= g . x by A7 ; ::_thesis: verum
end;
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
proof
A1: n in NAT by ORDINAL1:def_12;
for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
(CircleIso (p,r)) . a = (r * b) + p by Def6;
hence CircleIso (p,r) is being_homeomorphism by A1, TOPREALB:19; ::_thesis: verum
end;
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]|
proof
defpred S1[ real number , set ] means $2 = |[(cos ((2 * PI) * $1)),(sin ((2 * PI) * $1)),0]|;
A1: for x being Element of R^1 ex y being Element of (Tunit_circle 3) st S1[x,y]
proof
let x be Element of R^1; ::_thesis: ex y being Element of (Tunit_circle 3) st S1[x,y]
set y = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|;
|.(|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| - |[0,0,0]|).| = |.|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|.| by EUCLID_5:4, RLVECT_1:13
.= sqrt ((((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `1) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `2) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `3) ^2)) by Th35
.= sqrt ((((cos ((2 * PI) * x)) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `2) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `3) ^2)) by EUCLID_5:2
.= sqrt ((((cos ((2 * PI) * x)) ^2) + ((sin ((2 * PI) * x)) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `3) ^2)) by EUCLID_5:2
.= sqrt ((((cos ((2 * PI) * x)) ^2) + ((sin ((2 * PI) * x)) ^2)) + (Q ^2)) by EUCLID_5:2
.= 1 by SIN_COS:29, SQUARE_1:18 ;
then |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| is Element of (Tunit_circle 3) by Lm7, TOPREAL9:9;
hence ex y being Element of (Tunit_circle 3) st S1[x,y] ; ::_thesis: verum
end;
consider f being Function of the carrier of R^1,(Tunit_circle 3) such that
A2: for x being Element of R^1 holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take f ; ::_thesis: for x being real number holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|
let x be real number ; ::_thesis: f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|
x is Point of R^1 by TOPMETR:17, XREAL_0:def_1;
hence f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| by A2; ::_thesis: verum
end;
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
proof
let f, g be Function of R^1,(Tunit_circle 3); ::_thesis: ( ( for x being real number holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) & ( for x being real number holds g . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ) implies f = g )
assume that
A3: for x being real number holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| and
A4: for x being real number holds g . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| ; ::_thesis: f = g
let x be Point of R^1; :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x
thus f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| by A3
.= g . x by A4 ; ::_thesis: verum
end;
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]
proof
let i be Integer; ::_thesis: SphereMap . i = c[100]
thus SphereMap . i = |[(cos (((2 * PI) * i) + Q)),((sin ((2 * PI) * i)) + Q),0]| by Def7
.= |[(cos 0),(sin (((2 * PI) * i) + Q)),0]| by COMPLEX2:9
.= c[100] by COMPLEX2:8, SIN_COS:31 ; ::_thesis: verum
end;
Lm10: sin is Function of R^1,R^1
proof
A1: sin = R^1 sin ;
R^1 | (R^1 (dom sin)) = R^1 by SIN_COS:24, TOPREALB:6;
hence sin is Function of R^1,R^1 by A1, TOPREALA:7; ::_thesis: verum
end;
Lm11: cos is Function of R^1,R^1
proof
A1: cos = R^1 cos ;
R^1 | (R^1 (dom cos)) = R^1 by SIN_COS:24, TOPREALB:6;
hence cos is Function of R^1,R^1 by A1, TOPREALA:7; ::_thesis: verum
end;
Lm12: for r being real number holds SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]|
proof
let r be real number ; ::_thesis: SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]|
SphereMap . r = |[(cos (((2 * PI) * r) + Q)),(sin ((2 * PI) * r)),0]| by Def7
.= |[((cos * (AffineMap ((2 * PI),0))) . r),(sin (((2 * PI) * r) + Q)),0]| by TOPREALB:2
.= |[((cos * (AffineMap ((2 * PI),0))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| by TOPREALB:1 ;
hence SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| ; ::_thesis: verum
end;
registration
cluster SphereMap -> continuous ;
coherence
SphereMap is continuous
proof
A1: AffineMap ((2 * PI),0) = R^1 (AffineMap ((2 * PI),0)) ;
A2: R^1 | (R^1 (dom sin)) = R^1 by SIN_COS:24, TOPREALB:6;
A3: R^1 | (R^1 (dom cos)) = R^1 by SIN_COS:24, TOPREALB:6;
set sR = R^1 sin;
set cR = R^1 cos;
reconsider sR = R^1 sin, cR = R^1 cos as Function of R^1,R^1 by Lm10, Lm11;
reconsider l = AffineMap ((2 * PI),0) as Function of R^1,R^1 by TOPREALB:8;
A4: dom (AffineMap ((2 * PI),0)) = REAL by FUNCT_2:def_1;
A5: rng (AffineMap ((2 * PI),0)) = [#] REAL by FCONT_1:55;
set s = sR * l;
set c = cR * l;
reconsider g = SphereMap as Function of R^1,(TOP-REAL 3) by TOPREALA:7;
for p being Point of R^1
for V being Subset of (TOP-REAL 3) st g . p in V & V is open holds
ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )
proof
let p be Point of R^1; ::_thesis: for V being Subset of (TOP-REAL 3) st g . p in V & V is open holds
ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )
let V be Subset of (TOP-REAL 3); ::_thesis: ( g . p in V & V is open implies ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V ) )
assume that
A6: g . p in V and
A7: V is open ; ::_thesis: ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )
A8: V = Int V by A7, TOPS_1:23;
A9: ( (cR * l) . p is Real & (sR * l) . p is Real ) by XREAL_0:def_1;
reconsider e = g . p as Point of (Euclid 3) by TOPREAL3:8;
consider r being real number such that
A10: r > 0 and
A11: Ball (e,r) c= V by A6, A8, GOBOARD6:5;
set A = ].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[;
set B = ].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[;
set F = (1,2,3) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,{0});
A12: g . p = |[((cR * l) . p),((sR * l) . p),0]| by Lm12;
then A13: (g . p) `2 = (sR * l) . p by A9, EUCLID_5:2;
(g . p) `3 = 0 by A9, A12, EUCLID_5:2;
then A14: product ((1,2,3) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r) by Th48;
reconsider A = ].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[, B = ].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[ as Subset of R^1 by TOPMETR:17;
A15: A is open by JORDAN6:35;
A16: B is open by JORDAN6:35;
A17: sR is continuous by A2, PRE_TOPC:26;
(sR * l) . p in B by A10, A13, TOPREAL6:15;
then consider Ws being Subset of R^1 such that
A18: p in Ws and
A19: Ws is open and
A20: (sR * l) .: Ws c= B by A16, A17, A1, A4, A5, JGRAPH_2:10, TOPREALB:5;
A21: (g . p) `1 = (cR * l) . p by A12, A9, EUCLID_5:2;
A22: cR is continuous by A3, PRE_TOPC:26;
(cR * l) . p in A by A10, A21, TOPREAL6:15;
then consider Wc being Subset of R^1 such that
A23: p in Wc and
A24: Wc is open and
A25: (cR * l) .: Wc c= A by A15, A22, A1, A4, A5, JGRAPH_2:10, TOPREALB:5;
set W = Ws /\ Wc;
take Ws /\ Wc ; ::_thesis: ( p in Ws /\ Wc & Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus p in Ws /\ Wc by A18, A23, XBOOLE_0:def_4; ::_thesis: ( Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus Ws /\ Wc is open by A19, A24; ::_thesis: g .: (Ws /\ Wc) c= V
let y be Point of (TOP-REAL 3); :: according to LATTICE7:def_1 ::_thesis: ( not y in g .: (Ws /\ Wc) or y in V )
assume y in g .: (Ws /\ Wc) ; ::_thesis: y in V
then consider x being Element of R^1 such that
A26: x in Ws /\ Wc and
A27: y = g . x by FUNCT_2:65;
A28: g . x = |[((cR * l) . x),((sR * l) . x),0]| by Lm12;
x in Ws by A26, XBOOLE_0:def_4;
then A29: (sR * l) . x in (sR * l) .: Ws by FUNCT_2:35;
x in Wc by A26, XBOOLE_0:def_4;
then A30: (cR * l) . x in (cR * l) .: Wc by FUNCT_2:35;
|[((cR * l) . x),((sR * l) . x),0]| = (1,2,3) --> (((cR * l) . x),((sR * l) . x),0) by Th30;
then |[((cR * l) . x),((sR * l) . x),0]| in product ((1,2,3) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,{0})) by A20, A25, A29, A30, Lm2, Lm6, Th33;
then |[((cR * l) . x),((sR * l) . x),0]| in Ball (e,r) by A14;
hence y in V by A11, A27, A28; ::_thesis: verum
end;
then g is continuous by JGRAPH_2:10;
hence SphereMap is continuous by PRE_TOPC:27; ::_thesis: verum
end;
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]|
proof
defpred S1[ real number , set ] means $2 = |[(cos (((2 * PI) * r) * $1)),(sin (((2 * PI) * r) * $1)),0]|;
A1: for x being Element of I[01] ex y being Element of (Tunit_circle 3) st S1[x,y]
proof
let x be Element of I[01]; ::_thesis: ex y being Element of (Tunit_circle 3) st S1[x,y]
set y = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|;
|.(|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| - |[0,0,0]|).| = |.|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]|.| by EUCLID_5:4, RLVECT_1:13
.= sqrt ((((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `1) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `2) ^2)) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `3) ^2)) by Th35
.= sqrt ((((cos (((2 * PI) * r) * x)) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `2) ^2)) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `3) ^2)) by EUCLID_5:2
.= sqrt ((((cos (((2 * PI) * r) * x)) ^2) + ((sin (((2 * PI) * r) * x)) ^2)) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| `3) ^2)) by EUCLID_5:2
.= sqrt ((((cos (((2 * PI) * r) * x)) ^2) + ((sin (((2 * PI) * r) * x)) ^2)) + (Q ^2)) by EUCLID_5:2
.= 1 by SIN_COS:29, SQUARE_1:18 ;
then reconsider y = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| as Element of (Tunit_circle 3) by Lm7, TOPREAL9:9;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
ex f being Function of the carrier of I[01],(Tunit_circle 3) st
for x being Element of I[01] holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence 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]| ; ::_thesis: verum
end;
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
proof
let f, g be Function of I[01],(Tunit_circle 3); ::_thesis: ( ( for x being Point of I[01] holds f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) & ( for x being Point of I[01] holds g . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ) implies f = g )
assume that
A2: for x being Point of I[01] holds f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| and
A3: for x being Point of I[01] holds g . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ; ::_thesis: f = g
let x be Point of I[01]; :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x
thus f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| by A2
.= g . x by A3 ; ::_thesis: verum
end;
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)
proof
let r be real number ; ::_thesis: eLoop r = SphereMap * (ExtendInt r)
let x be Point of I[01]; :: according to FUNCT_2:def_8 ::_thesis: (eLoop r) . x = (SphereMap * (ExtendInt r)) . x
A1: (ExtendInt r) . x = r * x by TOPALG_5:def_1;
thus (eLoop r) . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| by Def8
.= |[(cos ((2 * PI) * ((ExtendInt r) . x))),(sin ((2 * PI) * ((ExtendInt r) . x))),0]| by A1
.= SphereMap . ((ExtendInt r) . x) by Def7
.= (SphereMap * (ExtendInt r)) . x by FUNCT_2:15 ; ::_thesis: verum
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
set f = eLoop i;
thus c[100] , c[100] are_connected ; :: according to BORSUK_2:def_2 ::_thesis: ( eLoop i is continuous & (eLoop i) . 0 = c[100] & (eLoop i) . 1 = c[100] )
eLoop i = SphereMap * (ExtendInt i) by Th62;
hence eLoop i is continuous ; ::_thesis: ( (eLoop i) . 0 = c[100] & (eLoop i) . 1 = c[100] )
thus (eLoop i) . 0 = |[(cos (((2 * PI) * i) * j0)),(sin (((2 * PI) * i) * j0)),0]| by Def8
.= c[100] by SIN_COS:31 ; ::_thesis: (eLoop i) . 1 = c[100]
thus (eLoop i) . 1 = |[(cos (((2 * PI) * i) * j1)),(sin (((2 * PI) * i) * j1)),0]| by Def8
.= |[(cos 0),(sin (((2 * PI) * i) + Q)),0]| by COMPLEX2:9
.= c[100] by COMPLEX2:8, SIN_COS:31 ; ::_thesis: verum
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
Tunit_circle 3 is having_trivial_Fundamental_Group by TOPALG_6:47;
hence for b1 being Loop of c[100] st b1 = eLoop i holds
b1 is nullhomotopic ; ::_thesis: verum
end;
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
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
|.(p (/) |.p.|).| = 1
let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) implies |.(p (/) |.p.|).| = 1 )
A1: |.p.| ^2 = Sum (sqr p) by TOPREAL9:5;
assume p <> 0. (TOP-REAL n) ; ::_thesis: |.(p (/) |.p.|).| = 1
then |.p.| <> 0 by EUCLID_2:42;
then Sum ((sqr p) (/) (Sum (sqr p))) = 1 by A1, Th20;
hence |.(p (/) |.p.|).| = 1 by A1, Th19, SQUARE_1:18; ::_thesis: verum
end;
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))
proof
A2: n in NAT by ORDINAL1:def_12;
|.((p (/) |.p.|) - (0. (TOP-REAL n))).| = |.(p (/) |.p.|).| by RLVECT_1:13
.= 1 by A1, Th63 ;
then p (/) |.p.| in Sphere ((0. (TOP-REAL n)),1) by A2, TOPREAL9:9;
hence p (/) |.p.| is Point of (Tcircle ((0. (TOP-REAL n)),1)) by A2, TOPREALB:9; ::_thesis: verum
end;
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))
proof
defpred S1[ Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)), set ] means for y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - $1 holds
$2 = Rn->S1 ((f . $1) - (f . y));
A1: for x being Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ex z being Element of (Tunit_circle n) st S1[x,z]
proof
let x be Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)); ::_thesis: ex z being Element of (Tunit_circle n) st S1[x,z]
reconsider y = - x as Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60;
reconsider z = Rn->S1 ((f . x) - (f . y)) as Point of (Tunit_circle n) ;
take z ; ::_thesis: S1[x,z]
thus S1[x,z] ; ::_thesis: verum
end;
ex g being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(Tunit_circle n) st
for x being Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) holds S1[x,g . x] from FUNCT_2:sch_3(A1);
hence 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)) ; ::_thesis: verum
end;
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
proof
let F, G be Function of (Tunit_circle (n + 1)),(Tunit_circle n); ::_thesis: ( ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
F . x = Rn->S1 ((f . x) - (f . y)) ) & ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
G . x = Rn->S1 ((f . x) - (f . y)) ) implies F = G )
assume that
A2: for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
F . x = Rn->S1 ((f . x) - (f . y)) and
A3: for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
G . x = Rn->S1 ((f . x) - (f . y)) ; ::_thesis: F = G
let p be Point of (Tunit_circle (n + 1)); :: according to FUNCT_2:def_8 ::_thesis: F . p = G . p
reconsider p2 = p as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ;
reconsider p1 = - p as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60;
thus F . p = Rn->S1 ((f . p2) - (f . p1)) by A2
.= G . p by A3 ; ::_thesis: verum
end;
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
proof
let n be non empty Nat; ::_thesis: 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
let r be real non negative number ; ::_thesis: 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
let x be Point of (TOP-REAL n); ::_thesis: ( x is Point of (Tcircle ((0. (TOP-REAL n)),r)) implies x, - x are_antipodals_of 0. (TOP-REAL n),r )
assume A1: x is Point of (Tcircle ((0. (TOP-REAL n)),r)) ; ::_thesis: x, - x are_antipodals_of 0. (TOP-REAL n),r
reconsider y = x as Point of (Tcircle ((0. (TOP-REAL n)),r)) by A1;
- x = - y ;
hence ( x is Point of (Tcircle ((0. (TOP-REAL n)),r)) & - x is Point of (Tcircle ((0. (TOP-REAL n)),r)) ) by TOPREALC:60; :: according to BORSUK_7:def_12 ::_thesis: 0. (TOP-REAL n) in LSeg (x,(- x))
((1 - (1 / 2)) * x) + ((1 / 2) * (- x)) = ((1 / 2) * x) + (- ((1 / 2) * x)) by EUCLID:40
.= 0. (TOP-REAL n) by EUCLID:36 ;
hence 0. (TOP-REAL n) in LSeg (x,(- x)) ; ::_thesis: verum
end;
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
proof
let n be non empty Nat; ::_thesis: 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
let p, x, y, x1, y1 be Point of (TOP-REAL n); ::_thesis: 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
let r be real positive number ; ::_thesis: ( x,y are_antipodals_of 0. (TOP-REAL n),1 & x1 = (CircleIso (p,r)) . x & y1 = (CircleIso (p,r)) . y implies x1,y1 are_antipodals_of p,r )
set h = CircleIso (p,r);
assume that
A1: x,y are_antipodals_of 0. (TOP-REAL n),1 and
A2: x1 = (CircleIso (p,r)) . x and
A3: y1 = (CircleIso (p,r)) . y ; ::_thesis: x1,y1 are_antipodals_of p,r
A4: x is Point of (Tcircle ((0. (TOP-REAL n)),1)) by A1, Def12;
hence x1 is Point of (Tcircle (p,r)) by A2, FUNCT_2:5; :: according to BORSUK_7:def_12 ::_thesis: ( y1 is Point of (Tcircle (p,r)) & p in LSeg (x1,y1) )
A5: y is Point of (Tcircle ((0. (TOP-REAL n)),1)) by A1, Def12;
hence y1 is Point of (Tcircle (p,r)) by A3, FUNCT_2:5; ::_thesis: p in LSeg (x1,y1)
0. (TOP-REAL n) in LSeg (x,y) by A1, Def12;
then consider a being Real such that
A6: 0. (TOP-REAL n) = ((1 - a) * x) + (a * y) and
A7: ( 0 <= a & a <= 1 ) ;
A8: (1 - a) * x1 = (1 - a) * ((r * x) + p) by A2, A4, Def6
.= ((1 - a) * (r * x)) + ((1 - a) * p) by EUCLID:32
.= ((r * (1 - a)) * x) + ((1 - a) * p) by EUCLID:30
.= (r * ((1 - a) * x)) + ((1 - a) * p) by EUCLID:30 ;
a * y1 = a * ((r * y) + p) by A3, A5, Def6
.= (a * (r * y)) + (a * p) by EUCLID:32
.= ((r * a) * y) + (a * p) by EUCLID:30
.= (r * (a * y)) + (a * p) by EUCLID:30 ;
then ((1 - a) * x1) + (a * y1) = (((r * ((1 - a) * x)) + ((1 - a) * p)) + (r * (a * y))) + (a * p) by A8, EUCLID:26
.= (((r * ((1 - a) * x)) + (r * (a * y))) + ((1 - a) * p)) + (a * p) by EUCLID:26
.= ((r * (((1 - a) * x) + (a * y))) + ((1 - a) * p)) + (a * p) by EUCLID:32
.= ((0. (TOP-REAL n)) + ((1 - a) * p)) + (a * p) by A6, EUCLID:28
.= ((1 - a) * p) + (a * p) by EUCLID:27
.= ((1 * p) - (a * p)) + (a * p) by EUCLID:50
.= 1 * p by EUCLID:48
.= p by EUCLID:29 ;
hence p in LSeg (x1,y1) by A7; ::_thesis: verum
end;
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)
proof
let n be non zero Nat; ::_thesis: 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)
set TC4 = Tcircle ((0. (TOP-REAL (n + 1))),1);
let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: 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)
let x be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); ::_thesis: ( f is without_antipodals implies (f . x) - (f . (- x)) <> 0. (TOP-REAL n) )
assume A1: f is without_antipodals ; ::_thesis: (f . x) - (f . (- x)) <> 0. (TOP-REAL n)
A2: dom f = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def_1;
reconsider y = - x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60;
reconsider a = x, b = y as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ;
reconsider x1 = x as Point of (TOP-REAL (n + 1)) by PRE_TOPC:25;
assume A3: (f . x) - (f . (- x)) = 0. (TOP-REAL n) ; ::_thesis: contradiction
x1, - x1 are_antipodals_of 0. (TOP-REAL (n + 1)),1,f
proof
thus x1, - x1 are_antipodals_of 0. (TOP-REAL (n + 1)),1 by Th64; :: according to BORSUK_7:def_13 ::_thesis: ( x1 in dom f & - x1 in dom f & f . x1 = f . (- x1) )
( f . x = f . a & f . y = f . b ) ;
hence ( x1 in dom f & - x1 in dom f ) by A2; ::_thesis: f . x1 = f . (- x1)
(f . a) - (f . y) = 0. (TOP-REAL n) by A3;
hence f . x1 = f . (- x1) by EUCLID:43; ::_thesis: verum
end;
hence contradiction by A1, Def14; ::_thesis: verum
end;
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
proof
let n be non zero Nat; ::_thesis: 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
set TC4 = Tcircle ((0. (TOP-REAL (n + 1))),1);
let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: ( f is without_antipodals implies Sn1->Sn f is odd )
assume A1: f is without_antipodals ; ::_thesis: Sn1->Sn f is odd
set g = Sn1->Sn f;
let x, y be complex-valued Function; :: according to BORSUK_7:def_2 ::_thesis: ( x in dom (Sn1->Sn f) & - x in dom (Sn1->Sn f) & y = (Sn1->Sn f) . x implies (Sn1->Sn f) . (- x) = - y )
assume that
A2: x in dom (Sn1->Sn f) and
A3: - x in dom (Sn1->Sn f) and
A4: y = (Sn1->Sn f) . x ; ::_thesis: (Sn1->Sn f) . (- x) = - y
reconsider b = - x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by A3;
reconsider a = - b as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by A2;
set p = (f . b) - (f . a);
set q = (f . a) - (f . b);
A5: (f . b) - (f . a) = - ((f . a) - (f . b)) by EUCLID:44;
A6: n in NAT by ORDINAL1:def_12;
0. (TOP-REAL n) = 0* n by EUCLID:70;
then A7: - ((f . b) - (f . a)) <> 0. (TOP-REAL n) by A1, Th66, Th15;
thus (Sn1->Sn f) . (- x) = Rn->S1 ((f . b) - (f . a)) by Def10
.= ((f . b) - (f . a)) (/) |.((f . b) - (f . a)).| by A1, Th66, Def9
.= ((f . b) - (f . a)) (/) |.(- ((f . a) - (f . b))).| by EUCLID:44
.= (- ((f . a) - (f . b))) (/) |.(- ((f . a) - (f . b))).| by EUCLID:44
.= - (((f . a) - (f . b)) (/) |.(- ((f . a) - (f . b))).|) by VALUED_2:30
.= - (((f . a) - (f . b)) (/) |.((f . a) - (f . b)).|) by A6, TOPRNS_1:26
.= - (Rn->S1 ((f . a) - (f . b))) by A5, A7, Def9
.= - y by A4, Def10 ; ::_thesis: verum
end;
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)
proof
let n be non zero Nat; ::_thesis: 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)
let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: for 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)
let g, B1 be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: ( g = f (-) & B1 = f <--> g & f is without_antipodals implies Sn1->Sn f = B1 ((n NormF) * B1) )
assume that
A1: g = f (-) and
A2: B1 = f <--> g and
A3: f is without_antipodals ; ::_thesis: Sn1->Sn f = B1 ((n NormF) * B1)
set T = Tcircle ((0. (TOP-REAL (n + 1))),1);
set B = Sn1->Sn f;
set B2 = (n NormF) * B1;
set BB = B1 ((n NormF) * B1);
set TC3 = Tunit_circle (n + 1);
A4: dom B1 = the carrier of (Tunit_circle (n + 1)) by FUNCT_2:def_1;
dom (n NormF) = the carrier of (TOP-REAL n) by FUNCT_2:def_1;
then rng B1 c= dom (n NormF) ;
then A5: dom ((n NormF) * B1) = dom B1 by RELAT_1:27;
A6: dom (B1 ((n NormF) * B1)) = (dom B1) /\ (dom ((n NormF) * B1)) by VALUED_2:71
.= the carrier of (Tunit_circle (n + 1)) by A5, FUNCT_2:def_1 ;
hence dom (Sn1->Sn f) = dom (B1 ((n NormF) * B1)) by FUNCT_2:def_1; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom (Sn1->Sn f) or (Sn1->Sn f) . b1 = (B1 ((n NormF) * B1)) . b1 )
let x be set ; ::_thesis: ( not x in dom (Sn1->Sn f) or (Sn1->Sn f) . x = (B1 ((n NormF) * B1)) . x )
assume x in dom (Sn1->Sn f) ; ::_thesis: (Sn1->Sn f) . x = (B1 ((n NormF) * B1)) . x
then reconsider x1 = x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ;
reconsider y1 = - x1 as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60;
set p = (f . x1) - (f . y1);
A7: dom g = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def_1;
A8: B1 . x1 = (f . x1) - (g . x1) by A4, A2, VALUED_2:def_46
.= (f . x1) - (f . y1) by A7, A1, VALUED_2:def_34 ;
A9: ((n NormF) * B1) . x1 = (n NormF) . (B1 . x1) by FUNCT_2:15
.= |.((f . x1) - (f . y1)).| by A8, JGRAPH_4:def_1 ;
(Sn1->Sn f) . x1 = Rn->S1 ((f . x1) - (f . y1)) by Def10
.= (B1 . x1) (/) (((n NormF) * B1) . x1) by A8, A9, A3, Th66, Def9
.= (B1 . x1) (#) ((((n NormF) * B1) ") . x1) by VALUED_1:10
.= (B1 ((n NormF) * B1)) . x1 by A6, VALUED_2:def_43 ;
hence (Sn1->Sn f) . x = (B1 ((n NormF) * B1)) . x ; ::_thesis: verum
end;
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
proof
let n be non zero Nat; ::_thesis: 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
set T = Tcircle ((0. (TOP-REAL (n + 1))),1);
let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); ::_thesis: ( f is without_antipodals & f is continuous implies Sn1->Sn f is continuous )
assume that
A1: f is without_antipodals and
A2: f is continuous ; ::_thesis: Sn1->Sn f is continuous
set B = Sn1->Sn f;
reconsider g = f (-) as Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:61;
reconsider B1 = f <--> g as Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:40;
set B2 = (n NormF) * B1;
A3: dom g = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def_1;
A4: dom B1 = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def_1;
A5: now__::_thesis:_for_t_being_Point_of_(Tcircle_((0._(TOP-REAL_(n_+_1))),1))_holds_((n_NormF)_*_B1)_._t_=_|.(B1_._t).|
let t be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); ::_thesis: ((n NormF) * B1) . t = |.(B1 . t).|
thus ((n NormF) * B1) . t = (n NormF) . (B1 . t) by FUNCT_2:15
.= |.(B1 . t).| by JGRAPH_4:def_1 ; ::_thesis: verum
end;
A6: now__::_thesis:_for_t_being_Point_of_(Tcircle_((0._(TOP-REAL_(n_+_1))),1))_holds_|.(B1_._t).|_<>_0
let t be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); ::_thesis: |.(B1 . t).| <> 0
A7: n in NAT by ORDINAL1:def_12;
A8: B1 . t = (f . t) - (g . t) by A4, VALUED_2:def_46
.= (f . t) - (f . (- t)) by A3, VALUED_2:def_34 ;
(f . t) - (f . (- t)) <> 0. (TOP-REAL n) by A1, Th66;
hence |.(B1 . t).| <> 0 by A8, A7, TOPRNS_1:24; ::_thesis: verum
end;
A9: (n NormF) * B1 is non-empty
proof
let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not x in dom ((n NormF) * B1) or not ((n NormF) * B1) . x is empty )
assume x in dom ((n NormF) * B1) ; ::_thesis: not ((n NormF) * B1) . x is empty
then reconsider x = x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ;
((n NormF) * B1) . x = |.(B1 . x).| by A5;
hence not ((n NormF) * B1) . x is empty by A6; ::_thesis: verum
end;
A10: g is continuous Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by A2, TOPREALC:62;
B1 ((n NormF) * B1) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:46;
hence Sn1->Sn f is continuous by A1, Th68, TOPMETR:6, A9, A2, A10; ::_thesis: verum
end;
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)
proof
let s be real number ; ::_thesis: 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)
let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: ( f is without_antipodals & 0 <= s & s <= 1 / 2 implies H1(f) . (s + (1 / 2)) = - (H1(f) . s) )
set l = eLoop 1;
set g = Sn1->Sn f;
set t = s + (1 / 2);
assume f is without_antipodals ; ::_thesis: ( not 0 <= s or not s <= 1 / 2 or H1(f) . (s + (1 / 2)) = - (H1(f) . s) )
then A1: Sn1->Sn f is odd by Th67;
assume A2: ( 0 <= s & s <= 1 / 2 ) ; ::_thesis: H1(f) . (s + (1 / 2)) = - (H1(f) . s)
then A3: s + (1 / 2) in the carrier of I[01] by Lm4;
reconsider s1 = s as Point of I[01] by A2, Lm3;
A4: dom (Sn1->Sn f) = the carrier of (Tunit_circle (2 + 1)) by FUNCT_2:def_1;
A5: - ((eLoop 1) . s1) is Point of (Tcircle ((0. (TOP-REAL 3)),1)) by TOPREALC:60;
A6: (eLoop 1) . (s + (1 / 2)) = |[(cos (((2 * PI) * 1) * (s + (1 / 2)))),(sin (((2 * PI) * 1) * (s + (1 / 2)))),0]| by A3, Def8
.= |[(- (cos ((2 * PI) * s))),(sin (((2 * PI) * s) + PI)),0]| by SIN_COS:79
.= |[(- (cos ((2 * PI) * s))),(- (sin ((2 * PI) * s))),(- Q)]| by SIN_COS:79
.= - |[(cos (((2 * PI) * 1) * s)),(sin (((2 * PI) * 1) * s)),0]| by EUCLID_5:11
.= - ((eLoop 1) . s1) by Def8 ;
thus H1(f) . (s + (1 / 2)) = (Sn1->Sn f) . ((eLoop 1) . (s + (1 / 2))) by A2, Lm4, FUNCT_2:15
.= - ((Sn1->Sn f) . ((eLoop 1) . s1)) by A1, A4, A5, A6, Def2
.= - (H1(f) . s1) by FUNCT_2:15
.= - (H1(f) . s) ; ::_thesis: verum
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_=_-_(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
proof
let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: ( f is without_antipodals & f is continuous implies H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a )
assume ( f is without_antipodals & f is continuous ) ; ::_thesis: H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a
then reconsider g = Sn1->Sn f as continuous Function of (Tunit_circle 3),(Tunit_circle 2) by Lm13;
H1(f) = g * (eLoop 1) ;
hence H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a ; ::_thesis: verum
end;
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 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 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 to TARSKI: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
proof
let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: 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
let xt be Point of R^1; ::_thesis: 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
let L be Loop of (Sn1->Sn f) . c100a; ::_thesis: ( L = H1(f) implies for I being Integer st S2[f,xt,I] holds
(liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I )
assume A1: L = H1(f) ; ::_thesis: for I being Integer st S2[f,xt,I] holds
(liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I
let I be Integer; ::_thesis: ( S2[f,xt,I] implies (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I )
assume A2: S2[f,xt,I] ; ::_thesis: (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . 0) + I
set l = liftPath (L,xt);
(1 / 2) + (1 / 2) = 1 ;
hence (liftPath (L,xt)) . 1 = ((liftPath (L,xt)) . (Q + (1 / 2))) + (I / 2) by A1, A2
.= (((liftPath (L,xt)) . 0) + (I / 2)) + (I / 2) by A1, A2
.= ((liftPath (L,xt)) . 0) + I ;
::_thesis: verum
end;
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
proof
let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: ( f is without_antipodals & f is continuous implies not H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a )
assume A1: ( f is without_antipodals & f is continuous ) ; ::_thesis: H1(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a
then reconsider L = H1(f) as Loop of (Sn1->Sn f) . c100a by Lm16;
set g = Sn1->Sn f;
set s = (Sn1->Sn f) . c100a;
not L is nullhomotopic
proof
let c be constant Loop of (Sn1->Sn f) . c100a; :: according to TOPALG_6:def_3 ::_thesis: not L,c are_homotopic
rng CircleMap = the carrier of (Tunit_circle 2) by FUNCT_2:def_3;
then consider xt being set such that
A2: xt in the carrier of R^1 and
A3: CircleMap . xt = (Sn1->Sn f) . c100a by FUNCT_2:11;
reconsider xt = xt as Point of R^1 by A2;
(Sn1->Sn f) . c100a in {((Sn1->Sn f) . c100a)} by TARSKI:def_1;
then A4: xt in CircleMap " {((Sn1->Sn f) . c100a)} by A3, FUNCT_2:38;
then consider q being odd Integer such that
A5: S2[f,xt,q] by A1, Lm18;
reconsider l = liftPath (L,xt) as continuous Function of I[01],R^1 by A4, Def11;
A6: l . 1 = (l . 0) + q by A5, Lm19;
A7: CircleMap . q = c[10] by TOPREALB:32;
A8: CircleMap . 0 = c[10] by TOPREALB:32;
set hh = l - xt;
l - xt is Path of R^1 0, R^1 q
proof
thus l - xt is continuous ; :: according to BORSUK_2:def_4 ::_thesis: ( (l - xt) . 0 = R^1 0 & (l - xt) . 1 = R^1 q )
thus (l - xt) . 0 = (l . j0) - xt by VALUED_1:4
.= xt - xt by A4, Def11
.= R^1 0 ; ::_thesis: (l - xt) . 1 = R^1 q
thus (l - xt) . 1 = (l . j1) - xt by VALUED_1:4
.= (xt + q) - xt by A6, A4, Def11
.= R^1 q ; ::_thesis: verum
end;
then reconsider hh = l - xt as Path of R^1 0, R^1 q ;
reconsider Ch = CircleMap * hh as Loop of c[10] by A7, TOPREALB:32;
reconsider X = I[01] --> xt as Loop of xt by JORDAN:41;
set xx = X - xt;
reconsider Cx = CircleMap * (X - xt) as Loop of c[10] by A8;
A9: dom Ciso = the carrier of INT.Group by FUNCT_2:def_1;
A10: Ciso . q = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * hh)) by TOPALG_5:25;
A11: Ciso . 0 = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * (X - xt))) by TOPALG_5:25;
Ciso . (@' 0) <> Ciso . (@' q) by A9, FUNCT_1:def_4;
then A12: not Cx,Ch are_homotopic by A10, A11, TOPALG_1:46;
assume L,c are_homotopic ; ::_thesis: contradiction
then consider F being Function of [:I[01],I[01]:],(Tunit_circle 2) such that
A13: F is continuous and
A14: for t being Point of I[01] holds
( F . (t,0) = H1(f) . t & F . (t,1) = c . t & F . (0,t) = (Sn1->Sn f) . c100a & F . (1,t) = (Sn1->Sn f) . c100a ) by BORSUK_2:def_7;
reconsider S = (Sn1->Sn f) . c100a as Point of (TOP-REAL 2) by PRE_TOPC:25;
set A = - (Arg S);
set H = RotateCircle (1,(- (Arg S)));
set G = (RotateCircle (1,(- (Arg S)))) * F;
A15: |.(euc2cpx S).| = |.S.| by EUCLID_3:25
.= 1 by TOPREALB:12 ;
A16: Rotate ((euc2cpx S),(- (Arg S))) = |.(euc2cpx S).| by COMPLEX2:55;
A17: (RotateCircle (1,(- (Arg S)))) . ((Sn1->Sn f) . c100a) = (Rotate (- (Arg S))) . S by FUNCT_1:49
.= c[10] by A16, A15, COMPLEX1:6, JORDAN24:def_3 ;
now__::_thesis:_for_t_being_Point_of_I[01]_holds_
(_((RotateCircle_(1,(-_(Arg_S))))_*_F)_._(t,0)_=_Ch_._t_&_((RotateCircle_(1,(-_(Arg_S))))_*_F)_._(t,1)_=_Cx_._t_&_((RotateCircle_(1,(-_(Arg_S))))_*_F)_._(0,t)_=_c[10]_&_((RotateCircle_(1,(-_(Arg_S))))_*_F)_._(1,t)_=_c[10]_)
let t be Point of I[01]; ::_thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = Ch . t & ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )
reconsider E = eLoop 1 as Function of I[01],(Tunit_circle (2 + 1)) ;
reconsider BU = H1(f) as Function of I[01],(Tunit_circle 2) ;
reconsider T = BU . t as Point of (TOP-REAL 2) by PRE_TOPC:25;
H1(f) = CircleMap * l by A4, Def11;
then A18: H1(f) . t = CircleMap . (l . t) by FUNCT_2:15;
thus ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = (RotateCircle (1,(- (Arg S)))) . (F . (t,j0)) by Lm1, BINOP_1:18
.= (RotateCircle (1,(- (Arg S)))) . T by A14
.= CircleMap . ((l . t) - xt) by A3, A18, Th60
.= CircleMap . (hh . t) by VALUED_1:4
.= Ch . t by FUNCT_2:15 ; ::_thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )
thus ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = (RotateCircle (1,(- (Arg S)))) . (F . (t,j1)) by Lm1, BINOP_1:18
.= (RotateCircle (1,(- (Arg S)))) . (c . t) by A14
.= (RotateCircle (1,(- (Arg S)))) . ((Sn1->Sn f) . c100a) by TOPALG_3:21
.= CircleMap . (xt - xt) by A17, TOPREALB:32
.= CircleMap . ((X . t) - xt) by TOPALG_3:21
.= CircleMap . ((X - xt) . t) by VALUED_1:4
.= Cx . t by FUNCT_2:15 ; ::_thesis: ( ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )
thus ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = (RotateCircle (1,(- (Arg S)))) . (F . (j0,t)) by Lm1, BINOP_1:18
.= c[10] by A14, A17 ; ::_thesis: ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10]
thus ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = (RotateCircle (1,(- (Arg S)))) . (F . (j1,t)) by Lm1, BINOP_1:18
.= c[10] by A14, A17 ; ::_thesis: verum
end;
hence contradiction by A12, A13, BORSUK_2:def_7; ::_thesis: verum
end;
hence H1(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a ; ::_thesis: verum
end;
Lm21: for f being continuous Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2) holds f is with_antipodals
proof
let f be continuous Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ::_thesis: f is with_antipodals
assume A1: not f is with_antipodals ; ::_thesis: contradiction
then H1(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a by Lm20;
hence contradiction by A1, Lm16; ::_thesis: verum
end;
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
proof
let f be Function of (Tcircle (p,r)),(TOP-REAL n); ::_thesis: f is without_antipodals
let x, y be Point of (TOP-REAL (n + 1)); :: according to BORSUK_7:def_14 ::_thesis: not x,y are_antipodals_of p,r,f
not x in dom f ;
hence not x,y are_antipodals_of p,r,f by Def13; ::_thesis: verum
end;
end;
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
proof
let f be Function of (Tcircle (p,r)),(TOP-REAL 2); ::_thesis: ( f is continuous implies f is with_antipodals )
assume A1: f is continuous ; ::_thesis: f is with_antipodals
A2: dom f = the carrier of (Tcircle (p,r)) by FUNCT_2:def_1;
percases ( r is positive or r is zero ) ;
suppose r is positive ; ::_thesis: f is with_antipodals
then reconsider r1 = r as real positive number ;
reconsider f1 = f as continuous Function of (Tcircle (p,r1)),(TOP-REAL 2) by A1;
reconsider h = CircleIso (p,r1) as Function of (Tcircle ((0. (TOP-REAL 3)),1)),(Tcircle (p,r1)) ;
f1 * h is with_antipodals by Lm21;
then consider x, y being Point of (TOP-REAL 3) such that
A3: x,y are_antipodals_of 0. (TOP-REAL 3),1,f1 * h by Def14;
A4: x in dom (f * h) by A3, Def13;
A5: y in dom (f * h) by A3, Def13;
A6: (f * h) . x = (f * h) . y by A3, Def13;
( h . x is Point of (Tcircle (p,r1)) & h . y is Point of (Tcircle (p,r1)) ) by A4, A5, FUNCT_2:5;
then reconsider hx = h . x, hy = h . y as Point of (TOP-REAL 3) by PRE_TOPC:25;
take hx ; :: according to BORSUK_7:def_14 ::_thesis: ex y being Point of (TOP-REAL 3) st hx,y are_antipodals_of p,r,f
take hy ; ::_thesis: hx,hy are_antipodals_of p,r,f
x,y are_antipodals_of 0. (TOP-REAL 3),1 by A3, Def13;
hence hx,hy are_antipodals_of p,r by Th65; :: according to BORSUK_7:def_13 ::_thesis: ( hx in dom f & hy in dom f & f . hx = f . hy )
thus hx in dom f by A2, A4, FUNCT_2:5; ::_thesis: ( hy in dom f & f . hx = f . hy )
thus hy in dom f by A2, A5, FUNCT_2:5; ::_thesis: f . hx = f . hy
thus f . hx = (f * h) . x by A4, FUNCT_2:15
.= f . hy by A5, A6, FUNCT_2:15 ; ::_thesis: verum
end;
supposeA7: r is zero ; ::_thesis: f is with_antipodals
take p ; :: according to BORSUK_7:def_14 ::_thesis: ex y being Point of (TOP-REAL 3) st p,y are_antipodals_of p,r,f
take p ; ::_thesis: p,p are_antipodals_of p,r,f
reconsider e = p as Point of (Euclid 3) by TOPREAL3:8;
A8: the carrier of (Tcircle (p,r)) = Sphere (p,r) by TOPREALB:9
.= Sphere (e,r) by TOPREAL9:15
.= {e} by A7, TOPREAL6:54 ;
thus p,p are_antipodals_of p,r :: according to BORSUK_7:def_13 ::_thesis: ( p in dom f & p in dom f & f . p = f . p )
proof
thus ( p is Point of (Tcircle (p,r)) & p is Point of (Tcircle (p,r)) ) by A8, TARSKI:def_1; :: according to BORSUK_7:def_12 ::_thesis: p in LSeg (p,p)
thus p in LSeg (p,p) by RLTOPSP1:68; ::_thesis: verum
end;
thus ( p in dom f & p in dom f ) by A2, A8, TARSKI:def_1; ::_thesis: f . p = f . p
thus f . p = f . p ; ::_thesis: verum
end;
end;
end;
end;
*