thus
CircleMap r is one-to-one
; ( CircleMap r is onto & CircleMap r is continuous )
thus
CircleMap r is onto
CircleMap r is continuous proof
set TOUC =
Topen_unit_circle (CircleMap . r);
set A =
].r,(r + 1).[;
set f =
CircleMap | ].r,(r + 1).[;
set X = the
carrier of
(Topen_unit_circle (CircleMap . r));
thus
rng (CircleMap r) c= the
carrier of
(Topen_unit_circle (CircleMap . r))
;
XBOOLE_0:def 10,
FUNCT_2:def 3 the carrier of (Topen_unit_circle (CircleMap . r)) c= rng (CircleMap r)
let y be
object ;
TARSKI:def 3 ( not y in the carrier of (Topen_unit_circle (CircleMap . r)) or y in rng (CircleMap r) )
A1:
[\r/] <= r
by INT_1:def 6;
A2:
dom (CircleMap | ].r,(r + 1).[) = ].r,(r + 1).[
by Lm18, RELAT_1:62;
assume A3:
y in the
carrier of
(Topen_unit_circle (CircleMap . r))
;
y in rng (CircleMap r)
then reconsider z =
y as
Point of
(TOP-REAL 2) by Lm8;
set z1 =
z `1 ;
set z2 =
z `2 ;
A4:
z `1 <= 1
by A3, Th26;
set x =
(arccos (z `1)) / (2 * PI);
A5:
- 1
<= z `1
by A3, Th26;
then A6:
0 <= (arccos (z `1)) / (2 * PI)
by A4, Lm22;
(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
(Tunit_circle 2)
by A3, PRE_TOPC:25;
then A10:
|.z.| = 1
by Th12;
per cases
( z `2 < 0 or z `2 >= 0 )
;
suppose A11:
z `2 < 0
;
y in rng (CircleMap r)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 A5, A4, SIN_COS6:91
.=
|[(z `1),(- (- (z `2)))]|
by A10, A9, A11, SIN_COS6:103
.=
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 A14:
not
(1 - ((arccos (z `1)) / (2 * PI))) + [\r/] in ].r,(r + 1).[
;
y in rng (CircleMap r)then
[\r/] - ((arccos (z `1)) / (2 * PI)) < r - 0
by A1, A6, XREAL_1:15;
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 A14, XXREAL_1:4;
([\r/] + 1) + 0 < ([\r/] + 1) + (1 - ((arccos (z `1)) / (2 * PI)))
by A8, XREAL_1:6;
then A16:
r < (2 - ((arccos (z `1)) / (2 * PI))) + [\r/]
by INT_1:29, XXREAL_0:2;
then
(1 - ((arccos (z `1)) / (2 * PI))) + [\r/] < r
by A15, XXREAL_0:1;
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 A16, XXREAL_1:4;
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 (CircleMap r)
by A2, A12, A17, FUNCT_1:def 3;
verum end; end; end; suppose A18:
z `2 >= 0
;
y in rng (CircleMap r)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 A5, A4, SIN_COS6:91
.=
|[(z `1),(z `2)]|
by A10, A9, A18, SIN_COS6:102
.=
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 A21:
not
((arccos (z `1)) / (2 * PI)) + [\r/] in ].r,(r + 1).[
;
y in rng (CircleMap r)
0 + ([\r/] + 1) <= ((arccos (z `1)) / (2 * PI)) + ([\r/] + 1)
by A6, XREAL_1:6;
then A22:
r < (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1
by INT_1:29, XXREAL_0:2;
((arccos (z `1)) / (2 * PI)) + [\r/] < 1
+ r
by A1, A7, XREAL_1:8;
then
((arccos (z `1)) / (2 * PI)) + [\r/] <= r
by A21, XXREAL_1:4;
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 A23, XXREAL_0:1;
then A24:
(((arccos (z `1)) / (2 * PI)) + [\r/]) + 1
in ].r,(r + 1).[
by A22, XXREAL_1:4;
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 (CircleMap r)
by A2, A19, A24, FUNCT_1:def 3;
verum end; end; end; end;
end;
Topen_unit_circle (CircleMap . r) = (Tunit_circle 2) | (([#] (Tunit_circle 2)) \ {(CircleMap . r)})
by Th22;
hence
CircleMap r is continuous
by TOPREALA:8; verum