set Z = R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[);
set I = ].0 ,p1.];
set J = [.p0,0 .[;
set K = [.(- 1),1.];
set h = (1 / (2 * PI )) (#) arccos ;
for p being Point of (Topen_unit_circle c[-10] ) holds Circle2IntervalL is_continuous_at p
proof
let p be
Point of
(Topen_unit_circle c[-10] );
:: thesis: Circle2IntervalL is_continuous_at p
consider x,
y being
real number such that A1:
p = |[x,y]|
and A2:
(
y >= 0 implies
Circle2IntervalL . p = 1
+ ((arccos x) / (2 * PI )) )
and A3:
(
y <= 0 implies
Circle2IntervalL . p = 1
- ((arccos x) / (2 * PI )) )
by Def14;
reconsider q =
p as
Point of
(TOP-REAL 2) by Lm9;
x = q `1
by A1, EUCLID:56;
then
(
- 1
<= x &
x <= 1 )
by Th27;
then A4:
x in [.(- 1),1.]
by XXREAL_1:1;
A5:
the
carrier of
(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) = ].(1 / 2),((1 / 2) + p1).[
by PRE_TOPC:29;
A6:
dom ((1 / (2 * PI )) (#) arccos ) = dom arccos
by VALUED_1:def 5;
then A7:
((1 / (2 * PI )) (#) arccos ) . x =
(arccos . x) * (1 / (2 * PI ))
by A4, SIN_COS6:88, VALUED_1:def 5
.=
(1 * (arccos . x)) / (2 * PI )
by XCMPLX_1:75
;
Tcircle (0.REAL 2),1 is
SubSpace of
Trectangle p0,
p1,
p0,
p1
by Th10;
then A9:
Topen_unit_circle c[-10] is
SubSpace of
Trectangle p0,
p1,
p0,
p1
by TSEP_1:7;
A10:
[.(- 1),1.] = [#] (Closed-Interval-TSpace (- 1),1)
by TOPMETR:25;
A11:
y = q `2
by A1, EUCLID:56;
per cases
( y = 0 or y < 0 or y > 0 )
;
suppose A12:
y < 0
;
:: thesis: Circle2IntervalL is_continuous_at p
for
V being
Subset of
(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) st
V is
open &
Circle2IntervalL . p in V holds
ex
W being
Subset of
(Topen_unit_circle c[-10] ) st
(
W is
open &
p in W &
Circle2IntervalL .: W c= V )
proof
let V be
Subset of
(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[));
:: thesis: ( V is open & Circle2IntervalL . p in V implies ex W being Subset of (Topen_unit_circle c[-10] ) st
( W is open & p in W & Circle2IntervalL .: W c= V ) )
assume that A13:
V is
open
and A14:
Circle2IntervalL . p in V
;
:: thesis: ex W being Subset of (Topen_unit_circle c[-10] ) st
( W is open & p in W & Circle2IntervalL .: W c= V )
A15:
Circle2IntervalL . p = 1
- ((arccos . x) / (2 * PI ))
by A3, A12, SIN_COS6:def 4;
reconsider V1 =
V as
Subset of
REAL by A5, XBOOLE_1:1;
reconsider V2 =
V1 as
Subset of
R^1 by TOPMETR:24;
V2 is
open
by A13, TSEP_1:17;
then reconsider V1 =
V1 as
open Subset of
REAL by BORSUK_5:62;
consider N1 being
Neighbourhood of
Circle2IntervalL . p such that A16:
N1 c= V1
by A14, RCOMP_1:39;
set hh =
h1 - ((1 / (2 * PI )) (#) arccos );
A17:
((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) . x = (h1 - ((1 / (2 * PI )) (#) arccos )) . x
by A4, FUNCT_1:72;
dom (h1 - ((1 / (2 * PI )) (#) arccos )) = (dom h1) /\ (dom ((1 / (2 * PI )) (#) arccos ))
by VALUED_1:12;
then A18:
dom (h1 - ((1 / (2 * PI )) (#) arccos )) =
REAL /\ (dom ((1 / (2 * PI )) (#) arccos ))
by FUNCOP_1:19
.=
[.(- 1),1.]
by A6, SIN_COS6:88, XBOOLE_1:28
;
then A19:
(h1 - ((1 / (2 * PI )) (#) arccos )) . x =
(h1 . x) - (((1 / (2 * PI )) (#) arccos ) . x)
by A4, VALUED_1:13
.=
1
- ((1 * (arccos . x)) / (2 * PI ))
by A4, A7, FUNCOP_1:13
;
Y:
x in dom ((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.])
by A18, A4, RELAT_1:86;
(h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.] is_continuous_in x
by Y, FCONT_1:def 2;
then consider N being
Neighbourhood of
x such that A20:
((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N c= N1
by A15, A17, A19, FCONT_1:5;
set N3 =
N /\ [.(- 1),1.];
A21:
N /\ [.(- 1),1.] c= [.(- 1),1.]
by XBOOLE_1:17;
reconsider N3 =
N /\ [.(- 1),1.],
J =
[.p0,0 .[ as
Subset of
(Closed-Interval-TSpace (- 1),1) by Lm2, XBOOLE_1:17, XXREAL_1:35;
set W =
(product (1,2 --> N3,J)) /\ the
carrier of
(Topen_unit_circle c[-10] );
y >= - 1
by A11, Th27;
then A22:
y in J
by A12, XXREAL_1:3;
A23:
p = 1,2
--> x,
y
by A1, TOPREALA:49;
reconsider W =
(product (1,2 --> N3,J)) /\ the
carrier of
(Topen_unit_circle c[-10] ) as
Subset of
(Topen_unit_circle c[-10] ) by XBOOLE_1:17;
take
W
;
:: thesis: ( W is open & p in W & Circle2IntervalL .: W c= V )
reconsider KK =
product (1,2 --> N3,J) as
Subset of
(Trectangle p0,p1,p0,p1) by TOPREALA:60;
R^1 N = N
;
then reconsider M3 =
N3 as
open Subset of
(Closed-Interval-TSpace (- 1),1) by A10, TOPS_2:32;
reconsider I3 =
J as
open Subset of
(Closed-Interval-TSpace (- 1),1) by TOPREALA:47;
KK = product (1,2 --> M3,I3)
;
then
KK is
open
by TOPREALA:61;
hence
W is
open
by A9, Lm18, TOPS_2:32;
:: thesis: ( p in W & Circle2IntervalL .: W c= V )
x in N
by RCOMP_1:37;
then
x in N3
by A4, XBOOLE_0:def 4;
then
p in product (1,2 --> N3,J)
by A22, A23, HILBERT3:11;
hence
p in W
by XBOOLE_0:def 4;
:: thesis: Circle2IntervalL .: W c= V
let m be
set ;
:: according to TARSKI:def 3 :: thesis: ( not m in Circle2IntervalL .: W or m in V )
assume
m in Circle2IntervalL .: W
;
:: thesis: m in V
then consider c being
Element of
(Topen_unit_circle c[-10] ) such that A24:
c in W
and A25:
m = Circle2IntervalL . c
by FUNCT_2:116;
consider c1,
c2 being
real number such that A26:
c = |[c1,c2]|
and
(
c2 >= 0 implies
Circle2IntervalL . c = 1
+ ((arccos c1) / (2 * PI )) )
and A27:
(
c2 <= 0 implies
Circle2IntervalL . c = 1
- ((arccos c1) / (2 * PI )) )
by Def14;
A28:
c in product (1,2 --> N3,J)
by A24, XBOOLE_0:def 4;
then A29:
c . 1
in N3
by TOPREALA:24;
A30:
dom ((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) = [.(- 1),1.]
by A18, RELAT_1:91;
A31:
((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N3 c= ((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N
by RELAT_1:156, XBOOLE_1:17;
A32:
((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) . (c . 1) =
(h1 - ((1 / (2 * PI )) (#) arccos )) . (c . 1)
by A21, A29, FUNCT_1:72
.=
(h1 . (c . 1)) - (((1 / (2 * PI )) (#) arccos ) . (c . 1))
by A18, A21, A29, VALUED_1:13
.=
1
- (((1 / (2 * PI )) (#) arccos ) . (c . 1))
by A29, FUNCOP_1:13
.=
1
- ((arccos . (c . 1)) * (1 / (2 * PI )))
by A6, A21, A29, SIN_COS6:88, VALUED_1:def 5
.=
1
- ((arccos . c1) * (1 / (2 * PI )))
by A26, TOPREALA:50
.=
1
- ((arccos c1) * (1 / (2 * PI )))
by SIN_COS6:def 4
;
c . 2
in J
by A28, TOPREALA:24;
then
c2 in J
by A26, TOPREALA:50;
then
1
- ((1 * (arccos c1)) * (1 / (2 * PI ))) = m
by A25, A27, XCMPLX_1:75, XXREAL_1:3;
then
m in ((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N3
by A21, A29, A30, A32, FUNCT_1:def 12;
then
m in ((h1 - ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N
by A31;
then
m in N1
by A20;
hence
m in V
by A16;
:: thesis: verum
end; hence
Circle2IntervalL is_continuous_at p
by TMAP_1:48;
:: thesis: verum suppose A33:
y > 0
;
:: thesis: Circle2IntervalL is_continuous_at p
for
V being
Subset of
(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) st
V is
open &
Circle2IntervalL . p in V holds
ex
W being
Subset of
(Topen_unit_circle c[-10] ) st
(
W is
open &
p in W &
Circle2IntervalL .: W c= V )
proof
let V be
Subset of
(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[));
:: thesis: ( V is open & Circle2IntervalL . p in V implies ex W being Subset of (Topen_unit_circle c[-10] ) st
( W is open & p in W & Circle2IntervalL .: W c= V ) )
assume that A34:
V is
open
and A35:
Circle2IntervalL . p in V
;
:: thesis: ex W being Subset of (Topen_unit_circle c[-10] ) st
( W is open & p in W & Circle2IntervalL .: W c= V )
A36:
Circle2IntervalL . p = 1
+ ((arccos . x) / (2 * PI ))
by A2, A33, SIN_COS6:def 4;
reconsider V1 =
V as
Subset of
REAL by A5, XBOOLE_1:1;
reconsider V2 =
V1 as
Subset of
R^1 by TOPMETR:24;
V2 is
open
by A34, TSEP_1:17;
then reconsider V1 =
V1 as
open Subset of
REAL by BORSUK_5:62;
consider N1 being
Neighbourhood of
Circle2IntervalL . p such that A37:
N1 c= V1
by A35, RCOMP_1:39;
set hh =
h1 + ((1 / (2 * PI )) (#) arccos );
A38:
((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) . x = (h1 + ((1 / (2 * PI )) (#) arccos )) . x
by A4, FUNCT_1:72;
dom (h1 + ((1 / (2 * PI )) (#) arccos )) = (dom h1) /\ (dom ((1 / (2 * PI )) (#) arccos ))
by VALUED_1:def 1;
then A39:
dom (h1 + ((1 / (2 * PI )) (#) arccos )) =
REAL /\ (dom ((1 / (2 * PI )) (#) arccos ))
by FUNCOP_1:19
.=
[.(- 1),1.]
by A6, SIN_COS6:88, XBOOLE_1:28
;
then A40:
(h1 + ((1 / (2 * PI )) (#) arccos )) . x =
(h1 . x) + (((1 / (2 * PI )) (#) arccos ) . x)
by A4, VALUED_1:def 1
.=
1
+ ((1 * (arccos . x)) / (2 * PI ))
by A4, A7, FUNCOP_1:13
;
Y:
x in dom ((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.])
by A39, A4, RELAT_1:86;
(h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.] is_continuous_in x
by Y, FCONT_1:def 2;
then consider N being
Neighbourhood of
x such that A41:
((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N c= N1
by A36, A38, A40, FCONT_1:5;
set N3 =
N /\ [.(- 1),1.];
A42:
N /\ [.(- 1),1.] c= [.(- 1),1.]
by XBOOLE_1:17;
reconsider N3 =
N /\ [.(- 1),1.],
I =
].0 ,p1.] as
Subset of
(Closed-Interval-TSpace (- 1),1) by Lm2, XBOOLE_1:17, XXREAL_1:36;
set W =
(product (1,2 --> N3,I)) /\ the
carrier of
(Topen_unit_circle c[-10] );
y <= 1
by A11, Th27;
then A43:
y in I
by A33, XXREAL_1:2;
A44:
p = 1,2
--> x,
y
by A1, TOPREALA:49;
reconsider W =
(product (1,2 --> N3,I)) /\ the
carrier of
(Topen_unit_circle c[-10] ) as
Subset of
(Topen_unit_circle c[-10] ) by XBOOLE_1:17;
take
W
;
:: thesis: ( W is open & p in W & Circle2IntervalL .: W c= V )
reconsider KK =
product (1,2 --> N3,I) as
Subset of
(Trectangle p0,p1,p0,p1) by TOPREALA:60;
R^1 N = N
;
then reconsider M3 =
N3 as
open Subset of
(Closed-Interval-TSpace (- 1),1) by A10, TOPS_2:32;
reconsider I3 =
I as
open Subset of
(Closed-Interval-TSpace (- 1),1) by TOPREALA:46;
KK = product (1,2 --> M3,I3)
;
then
KK is
open
by TOPREALA:61;
hence
W is
open
by A9, Lm18, TOPS_2:32;
:: thesis: ( p in W & Circle2IntervalL .: W c= V )
x in N
by RCOMP_1:37;
then
x in N3
by A4, XBOOLE_0:def 4;
then
p in product (1,2 --> N3,I)
by A43, A44, HILBERT3:11;
hence
p in W
by XBOOLE_0:def 4;
:: thesis: Circle2IntervalL .: W c= V
let m be
set ;
:: according to TARSKI:def 3 :: thesis: ( not m in Circle2IntervalL .: W or m in V )
assume
m in Circle2IntervalL .: W
;
:: thesis: m in V
then consider c being
Element of
(Topen_unit_circle c[-10] ) such that A45:
c in W
and A46:
m = Circle2IntervalL . c
by FUNCT_2:116;
consider c1,
c2 being
real number such that A47:
c = |[c1,c2]|
and A48:
(
c2 >= 0 implies
Circle2IntervalL . c = 1
+ ((arccos c1) / (2 * PI )) )
and
(
c2 <= 0 implies
Circle2IntervalL . c = 1
- ((arccos c1) / (2 * PI )) )
by Def14;
A49:
c in product (1,2 --> N3,I)
by A45, XBOOLE_0:def 4;
then A50:
c . 1
in N3
by TOPREALA:24;
A51:
dom ((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) = [.(- 1),1.]
by A39, RELAT_1:91;
A52:
((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N3 c= ((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N
by RELAT_1:156, XBOOLE_1:17;
A53:
((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) . (c . 1) =
(h1 + ((1 / (2 * PI )) (#) arccos )) . (c . 1)
by A42, A50, FUNCT_1:72
.=
(h1 . (c . 1)) + (((1 / (2 * PI )) (#) arccos ) . (c . 1))
by A39, A42, A50, VALUED_1:def 1
.=
1
+ (((1 / (2 * PI )) (#) arccos ) . (c . 1))
by A50, FUNCOP_1:13
.=
1
+ ((arccos . (c . 1)) * (1 / (2 * PI )))
by A6, A42, A50, SIN_COS6:88, VALUED_1:def 5
.=
1
+ ((arccos . c1) * (1 / (2 * PI )))
by A47, TOPREALA:50
.=
1
+ ((arccos c1) * (1 / (2 * PI )))
by SIN_COS6:def 4
;
c . 2
in I
by A49, TOPREALA:24;
then
c2 in I
by A47, TOPREALA:50;
then
1
+ ((1 * (arccos c1)) * (1 / (2 * PI ))) = m
by A46, A48, XCMPLX_1:75, XXREAL_1:2;
then
m in ((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N3
by A42, A50, A51, A53, FUNCT_1:def 12;
then
m in ((h1 + ((1 / (2 * PI )) (#) arccos )) | [.(- 1),1.]) .: N
by A52;
then
m in N1
by A41;
hence
m in V
by A37;
:: thesis: verum
end; hence
Circle2IntervalL is_continuous_at p
by TMAP_1:48;
:: thesis: verum
end;
hence
Circle2IntervalL is continuous
by TMAP_1:49; :: thesis: verum