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:18;
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:8;
consider x,
y being
Real 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:52;
A8:
x = q `1
by A4, EUCLID:52;
then A9:
x <= 1
by Th26;
- 1
<= x
by A8, Th26;
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:49;
dom ((1 / (2 * PI)) (#) arccos) =
dom arccos
by VALUED_1:def 5
.=
[.(- 1),1.]
by SIN_COS6:86
;
then
x in dom (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.])
by A10, RELAT_1:57;
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:86, VALUED_1:def 5
.=
(1 * (arccos . x)) / (2 * PI)
by XCMPLX_1:74
;
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:17;
V2 is
open
by A16, TSEP_1:17;
then reconsider V1 =
V1 as
open Subset of
REAL by BORSUK_5:39;
consider N1 being
Neighbourhood of
Circle2IntervalR . p such that A18:
N1 c= V1
by A17, RCOMP_1:18;
A19:
((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . x = (h1 - ((1 / (2 * PI)) (#) arccos)) . x
by A10, FUNCT_1:49;
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))
.=
[.(- 1),1.]
by A13, SIN_COS6:86, XBOOLE_1:28
;
then A21:
dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.]
by RELAT_1:62;
A22:
Circle2IntervalR . p = 1
- ((arccos . x) / (2 * PI))
by A6, A15, SIN_COS6:def 4;
A23:
p = (1,2)
--> (
x,
y)
by A4, TOPREALA:28;
x in dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.])
by A10, A20, RELAT_1:57;
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:7
;
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:38;
reconsider I3 =
J as
open Subset of
(Closed-Interval-TSpace ((- 1),1)) by TOPREALA:26;
A27:
((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N3 c= ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N
by RELAT_1:123, XBOOLE_1:17;
R^1 N = N
;
then reconsider M3 =
N3 as
open Subset of
(Closed-Interval-TSpace ((- 1),1)) by A2, TOPS_2:24;
KK = product ((1,2) --> (M3,I3))
;
then
KK is
open
by TOPREALA:39;
hence
W is
open
by A1, Lm16, TOPS_2:24;
( p in W & Circle2IntervalR .: W c= V )
x in N
by RCOMP_1:16;
then A28:
x in N3
by A10, XBOOLE_0:def 4;
y >= - 1
by A7, Th26;
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
object ;
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:65;
A31:
c in product ((1,2) --> (N3,J))
by A29, XBOOLE_0:def 4;
then A32:
c . 1
in N3
by TOPREALA:3;
consider c1,
c2 being
Real 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:3;
then
c2 in J
by A33, TOPREALA:29;
then A35:
1
- ((1 * (arccos c1)) * (1 / (2 * PI))) = m
by A30, A34, XCMPLX_1:74, XXREAL_1:3;
((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . (c . 1) =
(h1 - ((1 / (2 * PI)) (#) arccos)) . (c . 1)
by A26, A32, FUNCT_1:49
.=
(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:7
.=
1
- ((arccos . (c . 1)) * (1 / (2 * PI)))
by A13, A26, A32, SIN_COS6:86, VALUED_1:def 5
.=
1
- ((arccos . c1) * (1 / (2 * PI)))
by A33, TOPREALA:29
.=
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 6;
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:43;
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:17;
V2 is
open
by A37, TSEP_1:17;
then reconsider V1 =
V1 as
open Subset of
REAL by BORSUK_5:39;
consider N1 being
Neighbourhood of
Circle2IntervalR . p such that A39:
N1 c= V1
by A38, RCOMP_1:18;
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:38;
reconsider I3 =
I as
open Subset of
(Closed-Interval-TSpace ((- 1),1)) by TOPREALA:25;
A42:
(((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N3 c= (((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) .: N
by RELAT_1:123, XBOOLE_1:17;
R^1 N = N
;
then reconsider M3 =
N3 as
open Subset of
(Closed-Interval-TSpace ((- 1),1)) by A2, TOPS_2:24;
KK = product ((1,2) --> (M3,I3))
;
then
KK is
open
by TOPREALA:39;
hence
W is
open
by A1, Lm16, TOPS_2:24;
( p in W & Circle2IntervalR .: W c= V )
x in N
by RCOMP_1:16;
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:62, SIN_COS6:86;
A45:
p = (1,2)
--> (
x,
y)
by A4, TOPREALA:28;
y <= 1
by A7, Th26;
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
object ;
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:65;
A48:
c in product ((1,2) --> (N3,I))
by A46, XBOOLE_0:def 4;
then A49:
c . 1
in N3
by TOPREALA:3;
consider c1,
c2 being
Real 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:3;
then
c2 in I
by A50, TOPREALA:29;
then A52:
(1 * (arccos c1)) * (1 / (2 * PI)) = m
by A47, A51, XCMPLX_1:74, XXREAL_1:2;
(((1 / (2 * PI)) (#) arccos) | [.(- 1),1.]) . (c . 1) =
((1 / (2 * PI)) (#) arccos) . (c . 1)
by A41, A49, FUNCT_1:49
.=
(arccos . (c . 1)) * (1 / (2 * PI))
by A13, A41, A49, SIN_COS6:86, VALUED_1:def 5
.=
(arccos . c1) * (1 / (2 * PI))
by A50, TOPREALA:29
.=
(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 6;
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:43;
verum
end;
hence
Circle2IntervalR is continuous
by TMAP_1:44; verum