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