thus CircleMap r is one-to-one ; :: thesis: ( CircleMap r is onto & CircleMap r is continuous )
thus CircleMap r is onto :: thesis:
proof
set TOUC = Topen_unit_circle ();
set A = ].r,(r + 1).[;
set f = CircleMap | ].r,(r + 1).[;
set X = the carrier of ();
thus rng () c= the carrier of () ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of () c= rng ()
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of () or y in rng () )
A1: [\r/] <= r by INT_1:def 6;
A2: dom (CircleMap | ].r,(r + 1).[) = ].r,(r + 1).[ by ;
assume A3: y in the carrier of () ; :: thesis: y in rng ()
then reconsider z = y as Point of () by Lm8;
set z1 = z `1 ;
set z2 = z `2 ;
A4: z `1 <= 1 by ;
set x = (arccos (z `1)) / (2 * PI);
A5: - 1 <= z `1 by ;
then A6: 0 <= (arccos (z `1)) / (2 * PI) by ;
(arccos (z `1)) / (2 * PI) <= 1 / 2 by A5, A4, Lm22;
then A7: (arccos (z `1)) / (2 * PI) < 1 by XXREAL_0:2;
then A8: ((arccos (z `1)) / (2 * PI)) - ((arccos (z `1)) / (2 * PI)) < 1 - ((arccos (z `1)) / (2 * PI)) by XREAL_1:14;
A9: ((z `1) ^2) + ((z `2) ^2) = |.z.| ^2 by JGRAPH_1:29;
z is Point of () by ;
then A10: |.z.| = 1 by Th12;
per cases ( z `2 < 0 or z `2 >= 0 ) ;
suppose A11: z `2 < 0 ; :: thesis: y in rng ()
A12: CircleMap . (- ((arccos (z `1)) / (2 * PI))) = |[(cos (- ((2 * PI) * ((arccos (z `1)) / (2 * PI))))),(sin ((2 * PI) * (- ((arccos (z `1)) / (2 * PI)))))]| by Def11
.= |[(cos ((2 * PI) * ((arccos (z `1)) / (2 * PI)))),(sin ((2 * PI) * (- ((arccos (z `1)) / (2 * PI)))))]| by SIN_COS:31
.= |[(cos (arccos (z `1))),(sin (- ((2 * PI) * ((arccos (z `1)) / (2 * PI)))))]| by XCMPLX_1:87
.= |[(cos (arccos (z `1))),(- (sin ((2 * PI) * ((arccos (z `1)) / (2 * PI)))))]| by SIN_COS:31
.= |[(cos (arccos (z `1))),(- (sin (arccos (z `1))))]| by XCMPLX_1:87
.= |[(z `1),(- (sin (arccos (z `1))))]| by
.= |[(z `1),(- (- (z `2)))]| by
.= y by EUCLID:53 ;
per cases ( (1 - ((arccos (z `1)) / (2 * PI))) + [\r/] in ].r,(r + 1).[ or not (1 - ((arccos (z `1)) / (2 * PI))) + [\r/] in ].r,(r + 1).[ ) ;
suppose A13: (1 - ((arccos (z `1)) / (2 * PI))) + [\r/] in ].r,(r + 1).[ ; :: thesis: y in rng ()
then (CircleMap | ].r,(r + 1).[) . ((1 - ((arccos (z `1)) / (2 * PI))) + [\r/]) = CircleMap . ((- ((arccos (z `1)) / (2 * PI))) + ([\r/] + 1)) by FUNCT_1:49
.= CircleMap . (- ((arccos (z `1)) / (2 * PI))) by Th31 ;
hence y in rng () by ; :: thesis: verum
end;
suppose A14: not (1 - ((arccos (z `1)) / (2 * PI))) + [\r/] in ].r,(r + 1).[ ; :: thesis: y in rng ()
now :: thesis: not (arccos (z `1)) / (2 * PI) = 0
assume (arccos (z `1)) / (2 * PI) = 0 ; :: thesis: contradiction
then arccos (z `1) = 0 ;
then z `1 = 1 by ;
hence contradiction by A10, A9, A11; :: thesis: verum
end;
then [\r/] - ((arccos (z `1)) / (2 * PI)) < r - 0 by ;
then ((- ((arccos (z `1)) / (2 * PI))) + [\r/]) + 1 < r + 1 by XREAL_1:6;
then A15: r >= (1 - ((arccos (z `1)) / (2 * PI))) + [\r/] by ;
([\r/] + 1) + 0 < ([\r/] + 1) + (1 - ((arccos (z `1)) / (2 * PI))) by ;
then A16: r < (2 - ((arccos (z `1)) / (2 * PI))) + [\r/] by ;
now :: thesis: not ((- ((arccos (z `1)) / (2 * PI))) + [\r/]) + 1 = r
assume ((- ((arccos (z `1)) / (2 * PI))) + [\r/]) + 1 = r ; :: thesis: contradiction
then CircleMap . r = CircleMap . ((- ((arccos (z `1)) / (2 * PI))) + ([\r/] + 1))
.= CircleMap . (- ((arccos (z `1)) / (2 * PI))) by Th31 ;
hence contradiction by A3, A12, Th21; :: thesis: verum
end;
then (1 - ((arccos (z `1)) / (2 * PI))) + [\r/] < r by ;
then ((1 - ((arccos (z `1)) / (2 * PI))) + [\r/]) + 1 < r + 1 by XREAL_1:6;
then A17: ((- ((arccos (z `1)) / (2 * PI))) + [\r/]) + 2 in ].r,(r + 1).[ by ;
then (CircleMap | ].r,(r + 1).[) . ((- ((arccos (z `1)) / (2 * PI))) + ([\r/] + 2)) = CircleMap . ((- ((arccos (z `1)) / (2 * PI))) + ([\r/] + 2)) by FUNCT_1:49
.= CircleMap . (- ((arccos (z `1)) / (2 * PI))) by Th31 ;
hence y in rng () by ; :: thesis: verum
end;
end;
end;
suppose A18: z `2 >= 0 ; :: thesis: y in rng ()
A19: CircleMap . ((arccos (z `1)) / (2 * PI)) = |[(cos ((2 * PI) * ((arccos (z `1)) / (2 * PI)))),(sin ((2 * PI) * ((arccos (z `1)) / (2 * PI))))]| by Def11
.= |[(cos (arccos (z `1))),(sin ((2 * PI) * ((arccos (z `1)) / (2 * PI))))]| by XCMPLX_1:87
.= |[(cos (arccos (z `1))),(sin (arccos (z `1)))]| by XCMPLX_1:87
.= |[(z `1),(sin (arccos (z `1)))]| by
.= |[(z `1),(z `2)]| by
.= y by EUCLID:53 ;
per cases ( ((arccos (z `1)) / (2 * PI)) + [\r/] in ].r,(r + 1).[ or not ((arccos (z `1)) / (2 * PI)) + [\r/] in ].r,(r + 1).[ ) ;
suppose A20: ((arccos (z `1)) / (2 * PI)) + [\r/] in ].r,(r + 1).[ ; :: thesis: y in rng ()
then (CircleMap | ].r,(r + 1).[) . (((arccos (z `1)) / (2 * PI)) + [\r/]) = CircleMap . (((arccos (z `1)) / (2 * PI)) + [\r/]) by FUNCT_1:49
.= CircleMap . ((arccos (z `1)) / (2 * PI)) by Th31 ;
hence y in rng () by ; :: thesis: verum
end;
suppose A21: not ((arccos (z `1)) / (2 * PI)) + [\r/] in ].r,(r + 1).[ ; :: thesis: y in rng ()
0 + ([\r/] + 1) <= ((arccos (z `1)) / (2 * PI)) + ([\r/] + 1) by ;
then A22: r < (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1 by ;
A23: now :: thesis: not (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1 = r + 1
assume (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1 = r + 1 ; :: thesis: contradiction
then CircleMap . r = CircleMap . ((arccos (z `1)) / (2 * PI)) by Th31;
hence contradiction by A3, A19, Th21; :: thesis: verum
end;
((arccos (z `1)) / (2 * PI)) + [\r/] < 1 + r by ;
then ((arccos (z `1)) / (2 * PI)) + [\r/] <= r by ;
then (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1 <= r + 1 by XREAL_1:6;
then (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1 < r + 1 by ;
then A24: (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1 in ].r,(r + 1).[ by ;
then (CircleMap | ].r,(r + 1).[) . ((((arccos (z `1)) / (2 * PI)) + [\r/]) + 1) = CircleMap . (((arccos (z `1)) / (2 * PI)) + ([\r/] + 1)) by FUNCT_1:49
.= CircleMap . ((arccos (z `1)) / (2 * PI)) by Th31 ;
hence y in rng () by ; :: thesis: verum
end;
end;
end;
end;
end;
Topen_unit_circle () = () | (([#] ()) \ {()}) by Th22;
hence CircleMap r is continuous by TOPREALA:8; :: thesis: verum