begin
set P2 = 2 * PI;
set o = |[0,0]|;
set R = the carrier of R^1;
Lm1:
0 in INT
by INT_1:def 1;
reconsider p0 = - 1 as real negative number ;
reconsider p1 = 1 as real positive number ;
set CIT = Closed-Interval-TSpace ((- 1),1);
set cCIT = the carrier of (Closed-Interval-TSpace ((- 1),1));
Lm2:
the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.]
by TOPMETR:18;
Lm3:
1 - 0 <= 1
;
Lm4:
(3 / 2) - (1 / 2) <= 1
;
Lm5:
PI / 2 < PI / 1
by XREAL_1:76;
Lm6:
1 * PI < (3 / 2) * PI
by XREAL_1:68;
Lm7:
(3 / 2) * PI < 2 * PI
by XREAL_1:68;
Lm8:
for X being non empty TopSpace
for Y being non empty SubSpace of X
for Z being non empty SubSpace of Y
for p being Point of Z holds p is Point of X
Lm9:
for X being TopSpace
for Y being SubSpace of X
for Z being SubSpace of Y
for A being Subset of Z holds A is Subset of X
begin
Lm10:
sin is Function of R^1,R^1
Lm11:
cos is Function of R^1,R^1
set A = R^1 ].0,1.[;
Lm12:
now for a being non zero real number
for b being real number holds
( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) )
let a be non
zero real number ;
for b being real number holds
( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) )let b be
real number ;
( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) )A1:
rng (AffineMap (a,b)) = REAL
by FCONT_1:55;
A2:
[#] R^1 = REAL
by TOPMETR:17;
dom (AffineMap (a,b)) = REAL
by FUNCT_2:def 1;
hence
(
R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) &
R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) )
by A1, A2, TSEP_1:3;
verum
end;
begin
set TUC = Tunit_circle 2;
set cS1 = the carrier of (Tunit_circle 2);
Lm13:
the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1)
by Th9, EUCLID:54;
set TREC = Trectangle (p0,p1,p0,p1);
Lm14:
for n being non empty Element of NAT
for r being real positive number
for x being Point of (TOP-REAL n) holds Tunit_circle n, Tcircle (x,r) are_homeomorphic
Lm15:
c[10] <> c[-10]
by SPPOL_2:1;
set TOUC = Topen_unit_circle c[10];
set TOUCm = Topen_unit_circle c[-10];
set X = the carrier of (Topen_unit_circle c[10]);
set Xm = the carrier of (Topen_unit_circle c[-10]);
set Y = the carrier of (R^1 | (R^1 ].0,(0 + p1).[));
set Ym = the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[));
Lm16:
the carrier of (Topen_unit_circle c[10]) = [#] (Topen_unit_circle c[10])
;
Lm17:
the carrier of (Topen_unit_circle c[-10]) = [#] (Topen_unit_circle c[-10])
;
begin
Lm18:
dom CircleMap = REAL
by FUNCT_2:def 1, TOPMETR:17;
Lm19:
CircleMap . (1 / 2) = |[(- 1),0]|
Lm20:
for r being real number holds CircleMap . r = |[((cos * (AffineMap ((2 * PI),0))) . r),((sin * (AffineMap ((2 * PI),0))) . r)]|
Lm21:
for A being Subset of R^1 holds CircleMap | A is Function of (R^1 | A),(Tunit_circle 2)
Lm22:
for r being real number st - 1 <= r & r <= 1 holds
( 0 <= (arccos r) / (2 * PI) & (arccos r) / (2 * PI) <= 1 / 2 )
Lm23:
CircleMap | [.0,1.[ is one-to-one
Lm24:
for a, r being real number holds rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) = ].r,(r + 1).[
definition
existence
ex b1 being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) st
for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b1 . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) )
uniqueness
for b1, b2 being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) st ( for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b1 . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) ) ) & ( for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b2 . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b2 . p = 1 - ((arccos x) / (2 * PI)) ) ) ) holds
b1 = b2
end;
set A1 = R^1 ].(1 / 2),((1 / 2) + p1).[;
definition
existence
ex b1 being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st
for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) )
uniqueness
for b1, b2 being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st ( for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) ) ) & ( for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b2 . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b2 . p = 1 - ((arccos x) / (2 * PI)) ) ) ) holds
b1 = b2
end;
set C = Circle2IntervalR ;
set Cm = Circle2IntervalL ;
set A = ].0,1.[;
set Q = [.(- 1),1.[;
set E = ].0,PI.];
set j = 1 / (2 * PI);
reconsider Q = [.(- 1),1.[, E = ].0,PI.] as non empty Subset of REAL ;
Lm25:
the carrier of (R^1 | (R^1 Q)) = R^1 Q
by PRE_TOPC:8;
Lm26:
the carrier of (R^1 | (R^1 E)) = R^1 E
by PRE_TOPC:8;
Lm27:
the carrier of (R^1 | (R^1 ].0,1.[)) = R^1 ].0,1.[
by PRE_TOPC:8;
set Af = (AffineMap ((1 / (2 * PI)),0)) | (R^1 E);
dom (AffineMap ((1 / (2 * PI)),0)) = the carrier of R^1
by FUNCT_2:def 1, TOPMETR:17;
then Lm28:
dom ((AffineMap ((1 / (2 * PI)),0)) | (R^1 E)) = R^1 E
by RELAT_1:62;
rng ((AffineMap ((1 / (2 * PI)),0)) | (R^1 E)) c= ].0,1.[
then reconsider Af = (AffineMap ((1 / (2 * PI)),0)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].0,1.[)) by Lm26, Lm27, Lm28, FUNCT_2:2;
Lm29:
R^1 (AffineMap ((1 / (2 * PI)),0)) = AffineMap ((1 / (2 * PI)),0)
;
Lm30:
dom (AffineMap ((1 / (2 * PI)),0)) = REAL
by FUNCT_2:def 1;
Lm31:
rng (AffineMap ((1 / (2 * PI)),0)) = REAL
by FCONT_1:55;
R^1 | ([#] R^1) = R^1
by TSEP_1:3;
then reconsider Af = Af as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].0,1.[)) by Lm29, Lm30, Lm31, TOPMETR:17, TOPREALA:8;
set L = (R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[);
Lm32:
dom (AffineMap ((- 1),1)) = REAL
by FUNCT_2:def 1;
then Lm33:
dom ((R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[)) = ].0,1.[
by RELAT_1:62;
rng ((R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[)) c= ].0,1.[
then reconsider L = (R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[) as Function of (R^1 | (R^1 ].0,1.[)),(R^1 | (R^1 ].0,1.[)) by Lm27, Lm33, FUNCT_2:2;
Lm34:
rng (AffineMap ((- 1),1)) = REAL
by FCONT_1:55;
Lm35:
R^1 | ([#] R^1) = R^1
by TSEP_1:3;
then reconsider L = L as continuous Function of (R^1 | (R^1 ].0,1.[)),(R^1 | (R^1 ].0,1.[)) by Lm32, Lm34, TOPMETR:17, TOPREALA:8;
reconsider ac = R^1 arccos as continuous Function of (R^1 | (R^1 [.(- 1),1.])),(R^1 | (R^1 [.0,PI.])) by SIN_COS6:85, SIN_COS6:86;
set c = ac | (R^1 Q);
Lm36:
dom (ac | (R^1 Q)) = Q
by RELAT_1:62, SIN_COS6:86, XXREAL_1:35;
Lm37:
rng (ac | (R^1 Q)) c= E
then reconsider c = ac | (R^1 Q) as Function of (R^1 | (R^1 Q)),(R^1 | (R^1 E)) by Lm25, Lm26, Lm36, FUNCT_2:2;
the carrier of (R^1 | (R^1 [.(- 1),1.])) = [.(- 1),1.]
by PRE_TOPC:8;
then reconsider QQ = R^1 Q as Subset of (R^1 | (R^1 [.(- 1),1.])) by XXREAL_1:35;
the carrier of (R^1 | (R^1 [.0,PI.])) = [.0,PI.]
by PRE_TOPC:8;
then reconsider EE = R^1 E as Subset of (R^1 | (R^1 [.0,PI.])) by XXREAL_1:36;
Lm38:
(R^1 | (R^1 [.(- 1),1.])) | QQ = R^1 | (R^1 Q)
by GOBOARD9:2;
(R^1 | (R^1 [.0,PI.])) | EE = R^1 | (R^1 E)
by GOBOARD9:2;
then Lm39:
c is continuous
by Lm38, TOPREALA:8;
reconsider p = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
Lm40:
dom p = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm41:
p is continuous
by JORDAN5A:27;
Lm42:
for aX1 being Subset of (Topen_unit_circle c[10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[10]) & 0 <= q `2 ) } holds
Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous
Lm43:
for aX1 being Subset of (Topen_unit_circle c[10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[10]) & 0 >= q `2 ) } holds
Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous
Lm44:
for p being Point of (Topen_unit_circle c[10]) st p = c[-10] holds
Circle2IntervalR is_continuous_at p
set h1 = REAL --> 1;
reconsider h1 = REAL --> 1 as PartFunc of REAL,REAL ;
Lm45:
Circle2IntervalR is continuous
set A = ].(1 / 2),((1 / 2) + p1).[;
set Q = ].(- 1),1.];
set E = [.0,PI.[;
reconsider Q = ].(- 1),1.], E = [.0,PI.[ as non empty Subset of REAL ;
Lm46:
the carrier of (R^1 | (R^1 Q)) = R^1 Q
by PRE_TOPC:8;
Lm47:
the carrier of (R^1 | (R^1 E)) = R^1 E
by PRE_TOPC:8;
Lm48:
the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) = R^1 ].(1 / 2),((1 / 2) + p1).[
by PRE_TOPC:8;
set Af = (AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E);
dom (AffineMap ((- (1 / (2 * PI))),1)) = the carrier of R^1
by FUNCT_2:def 1, TOPMETR:17;
then Lm49:
dom ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) = R^1 E
by RELAT_1:62;
rng ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) c= ].(1 / 2),((1 / 2) + p1).[
then reconsider Af = (AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm47, Lm48, Lm49, FUNCT_2:2;
Lm50:
R^1 (AffineMap ((- (1 / (2 * PI))),1)) = AffineMap ((- (1 / (2 * PI))),1)
;
Lm51:
dom (AffineMap ((- (1 / (2 * PI))),1)) = REAL
by FUNCT_2:def 1;
rng (AffineMap ((- (1 / (2 * PI))),1)) = REAL
by FCONT_1:55;
then reconsider Af = Af as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm35, Lm50, Lm51, TOPMETR:17, TOPREALA:8;
set Af1 = (AffineMap ((1 / (2 * PI)),1)) | (R^1 E);
dom (AffineMap ((1 / (2 * PI)),1)) = the carrier of R^1
by FUNCT_2:def 1, TOPMETR:17;
then Lm52:
dom ((AffineMap ((1 / (2 * PI)),1)) | (R^1 E)) = R^1 E
by RELAT_1:62;
rng ((AffineMap ((1 / (2 * PI)),1)) | (R^1 E)) c= ].(1 / 2),((1 / 2) + p1).[
then reconsider Af1 = (AffineMap ((1 / (2 * PI)),1)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm47, Lm48, Lm52, FUNCT_2:2;
Lm53:
R^1 (AffineMap ((1 / (2 * PI)),1)) = AffineMap ((1 / (2 * PI)),1)
;
Lm54:
dom (AffineMap ((1 / (2 * PI)),1)) = REAL
by FUNCT_2:def 1;
rng (AffineMap ((1 / (2 * PI)),1)) = REAL
by FCONT_1:55;
then reconsider Af1 = Af1 as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm35, Lm53, Lm54, TOPMETR:17, TOPREALA:8;
set c = ac | (R^1 Q);
Lm55:
dom (ac | (R^1 Q)) = Q
by RELAT_1:62, SIN_COS6:86, XXREAL_1:36;
Lm56:
rng (ac | (R^1 Q)) c= E
then reconsider c = ac | (R^1 Q) as Function of (R^1 | (R^1 Q)),(R^1 | (R^1 E)) by Lm46, Lm47, Lm55, FUNCT_2:2;
the carrier of (R^1 | (R^1 [.(- 1),1.])) = [.(- 1),1.]
by PRE_TOPC:8;
then reconsider QQ = R^1 Q as Subset of (R^1 | (R^1 [.(- 1),1.])) by XXREAL_1:36;
the carrier of (R^1 | (R^1 [.0,PI.])) = [.0,PI.]
by PRE_TOPC:8;
then reconsider EE = R^1 E as Subset of (R^1 | (R^1 [.0,PI.])) by XXREAL_1:35;
Lm57:
(R^1 | (R^1 [.(- 1),1.])) | QQ = R^1 | (R^1 Q)
by GOBOARD9:2;
(R^1 | (R^1 [.0,PI.])) | EE = R^1 | (R^1 E)
by GOBOARD9:2;
then Lm58:
c is continuous
by Lm57, TOPREALA:8;
Lm59:
for aX1 being Subset of (Topen_unit_circle c[-10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 <= q `2 ) } holds
Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous
Lm60:
for aX1 being Subset of (Topen_unit_circle c[-10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) } holds
Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous
Lm61:
for p being Point of (Topen_unit_circle c[-10]) st p = c[10] holds
Circle2IntervalL is_continuous_at p
Lm62:
Circle2IntervalL is continuous
Lm63:
CircleMap (R^1 0) is open
Lm64:
CircleMap (R^1 (1 / 2)) is open
by Lm19, Th43, TOPREALA:14;
theorem
ex
F being
Subset-Family of
(Tunit_circle 2) st
(
F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} &
F is
Cover of
(Tunit_circle 2) &
F is
open & ( for
U being
Subset of
(Tunit_circle 2) holds
( (
U = CircleMap .: ].0,1.[ implies (
union (IntIntervals (0,1)) = CircleMap " U & ( for
d being
Subset of
R^1 st
d in IntIntervals (
0,1) holds
for
f being
Function of
(R^1 | d),
((Tunit_circle 2) | U) st
f = CircleMap | d holds
f is
being_homeomorphism ) ) ) & (
U = CircleMap .: ].(1 / 2),(3 / 2).[ implies (
union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for
d being
Subset of
R^1 st
d in IntIntervals (
(1 / 2),
(3 / 2)) holds
for
f being
Function of
(R^1 | d),
((Tunit_circle 2) | U) st
f = CircleMap | d holds
f is
being_homeomorphism ) ) ) ) ) )