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