set h = (1 / (2 * PI)) (#) arccos;
set K = [.(- 1),1.];
set J = [.p0,0.[;
set I = ].0,p1.];
set Z = R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[);
for p being Point of (Topen_unit_circle c[-10]) holds Circle2IntervalL 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]);
Circle2IntervalL 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 ].(1 / 2),((1 / 2) + p1).[)) = ].(1 / 2),((1 / 2) + p1).[
by PRE_TOPC:8;
consider x,
y being
Real such that A4:
p = |[x,y]|
and A5:
(
y >= 0 implies
Circle2IntervalL . p = 1
+ ((arccos x) / (2 * PI)) )
and A6:
(
y <= 0 implies
Circle2IntervalL . p = 1
- ((arccos x) / (2 * PI)) )
by Def14;
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;
A11:
dom ((1 / (2 * PI)) (#) arccos) = dom arccos
by VALUED_1:def 5;
then A12:
((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 A13:
y < 0
;
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
set hh =
h1 - ((1 / (2 * PI)) (#) arccos);
let V be
Subset of
(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[));
( 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 A14:
V is
open
and A15:
Circle2IntervalL . p in V
;
ex W being Subset of (Topen_unit_circle c[-10]) st
( W is open & p in W & Circle2IntervalL .: 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 A14, TSEP_1:17;
then reconsider V1 =
V1 as
open Subset of
REAL by BORSUK_5:39;
consider N1 being
Neighbourhood of
Circle2IntervalL . p such that A16:
N1 c= V1
by A15, RCOMP_1:18;
A17:
((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 A18:
dom (h1 - ((1 / (2 * PI)) (#) arccos)) =
REAL /\ (dom ((1 / (2 * PI)) (#) arccos))
.=
[.(- 1),1.]
by A11, SIN_COS6:86, XBOOLE_1:28
;
then A19:
dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.]
by RELAT_1:62;
A20:
Circle2IntervalL . p = 1
- ((arccos . x) / (2 * PI))
by A6, A13, SIN_COS6:def 4;
A21:
p = (1,2)
--> (
x,
y)
by A4, TOPREALA:28;
x in dom ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.])
by A10, A18, RELAT_1:57;
then A22:
(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, A18, VALUED_1:13
.=
1
- ((1 * (arccos . x)) / (2 * PI))
by A10, A12, FUNCOP_1:7
;
then consider N being
Neighbourhood of
x such that A23:
((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1
by A20, A17, A22, FCONT_1:5;
set N3 =
N /\ [.(- 1),1.];
A24:
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 & Circle2IntervalL .: 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;
A25:
((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, Lm17, TOPS_2:24;
( p in W & Circle2IntervalL .: W c= V )
x in N
by RCOMP_1:16;
then A26:
x in N3
by A10, XBOOLE_0:def 4;
y >= - 1
by A7, Th26;
then
y in J
by A13, XXREAL_1:3;
then
p in product ((1,2) --> (N3,J))
by A21, A26, HILBERT3:11;
hence
p in W
by XBOOLE_0:def 4;
Circle2IntervalL .: W c= V
let m be
object ;
TARSKI:def 3 ( not m in Circle2IntervalL .: W or m in V )
assume
m in Circle2IntervalL .: W
;
m in V
then consider c being
Element of
(Topen_unit_circle c[-10]) such that A27:
c in W
and A28:
m = Circle2IntervalL . c
by FUNCT_2:65;
A29:
c in product ((1,2) --> (N3,J))
by A27, XBOOLE_0:def 4;
then A30:
c . 1
in N3
by TOPREALA:3;
consider c1,
c2 being
Real such that A31:
c = |[c1,c2]|
and
(
c2 >= 0 implies
Circle2IntervalL . c = 1
+ ((arccos c1) / (2 * PI)) )
and A32:
(
c2 <= 0 implies
Circle2IntervalL . c = 1
- ((arccos c1) / (2 * PI)) )
by Def14;
c . 2
in J
by A29, TOPREALA:3;
then
c2 in J
by A31, TOPREALA:29;
then A33:
1
- ((1 * (arccos c1)) * (1 / (2 * PI))) = m
by A28, A32, XCMPLX_1:74, XXREAL_1:3;
((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . (c . 1) =
(h1 - ((1 / (2 * PI)) (#) arccos)) . (c . 1)
by A24, A30, FUNCT_1:49
.=
(h1 . (c . 1)) - (((1 / (2 * PI)) (#) arccos) . (c . 1))
by A18, A24, A30, VALUED_1:13
.=
1
- (((1 / (2 * PI)) (#) arccos) . (c . 1))
by A30, FUNCOP_1:7
.=
1
- ((arccos . (c . 1)) * (1 / (2 * PI)))
by A11, A24, A30, SIN_COS6:86, VALUED_1:def 5
.=
1
- ((arccos . c1) * (1 / (2 * PI)))
by A31, 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 A24, A30, A19, A33, FUNCT_1:def 6;
then
m in ((h1 - ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N
by A25;
then
m in N1
by A23;
hence
m in V
by A16;
verum
end; hence
Circle2IntervalL is_continuous_at p
by TMAP_1:43;
verum suppose A34:
y > 0
;
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
set hh =
h1 + ((1 / (2 * PI)) (#) arccos);
let V be
Subset of
(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[));
( 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 A35:
V is
open
and A36:
Circle2IntervalL . p in V
;
ex W being Subset of (Topen_unit_circle c[-10]) st
( W is open & p in W & Circle2IntervalL .: 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 A35, TSEP_1:17;
then reconsider V1 =
V1 as
open Subset of
REAL by BORSUK_5:39;
consider N1 being
Neighbourhood of
Circle2IntervalL . p such that A37:
N1 c= V1
by A36, RCOMP_1:18;
A38:
((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:def 1;
then A39:
dom (h1 + ((1 / (2 * PI)) (#) arccos)) =
REAL /\ (dom ((1 / (2 * PI)) (#) arccos))
.=
[.(- 1),1.]
by A11, SIN_COS6:86, XBOOLE_1:28
;
then A40:
dom ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) = [.(- 1),1.]
by RELAT_1:62;
A41:
Circle2IntervalL . p = 1
+ ((arccos . x) / (2 * PI))
by A5, A34, SIN_COS6:def 4;
A42:
p = (1,2)
--> (
x,
y)
by A4, TOPREALA:28;
x in dom ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.])
by A10, A39, RELAT_1:57;
then A43:
(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, A39, VALUED_1:def 1
.=
1
+ ((1 * (arccos . x)) / (2 * PI))
by A10, A12, FUNCOP_1:7
;
then consider N being
Neighbourhood of
x such that A44:
((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N c= N1
by A41, A38, A43, FCONT_1:5;
set N3 =
N /\ [.(- 1),1.];
A45:
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 & Circle2IntervalL .: 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;
A46:
((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, Lm17, TOPS_2:24;
( p in W & Circle2IntervalL .: W c= V )
x in N
by RCOMP_1:16;
then A47:
x in N3
by A10, XBOOLE_0:def 4;
y <= 1
by A7, Th26;
then
y in I
by A34, XXREAL_1:2;
then
p in product ((1,2) --> (N3,I))
by A42, A47, HILBERT3:11;
hence
p in W
by XBOOLE_0:def 4;
Circle2IntervalL .: W c= V
let m be
object ;
TARSKI:def 3 ( not m in Circle2IntervalL .: W or m in V )
assume
m in Circle2IntervalL .: W
;
m in V
then consider c being
Element of
(Topen_unit_circle c[-10]) such that A48:
c in W
and A49:
m = Circle2IntervalL . c
by FUNCT_2:65;
A50:
c in product ((1,2) --> (N3,I))
by A48, XBOOLE_0:def 4;
then A51:
c . 1
in N3
by TOPREALA:3;
consider c1,
c2 being
Real such that A52:
c = |[c1,c2]|
and A53:
(
c2 >= 0 implies
Circle2IntervalL . c = 1
+ ((arccos c1) / (2 * PI)) )
and
(
c2 <= 0 implies
Circle2IntervalL . c = 1
- ((arccos c1) / (2 * PI)) )
by Def14;
c . 2
in I
by A50, TOPREALA:3;
then
c2 in I
by A52, TOPREALA:29;
then A54:
1
+ ((1 * (arccos c1)) * (1 / (2 * PI))) = m
by A49, A53, XCMPLX_1:74, XXREAL_1:2;
((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) . (c . 1) =
(h1 + ((1 / (2 * PI)) (#) arccos)) . (c . 1)
by A45, A51, FUNCT_1:49
.=
(h1 . (c . 1)) + (((1 / (2 * PI)) (#) arccos) . (c . 1))
by A39, A45, A51, VALUED_1:def 1
.=
1
+ (((1 / (2 * PI)) (#) arccos) . (c . 1))
by A51, FUNCOP_1:7
.=
1
+ ((arccos . (c . 1)) * (1 / (2 * PI)))
by A11, A45, A51, SIN_COS6:86, VALUED_1:def 5
.=
1
+ ((arccos . c1) * (1 / (2 * PI)))
by A52, 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 A45, A51, A40, A54, FUNCT_1:def 6;
then
m in ((h1 + ((1 / (2 * PI)) (#) arccos)) | [.(- 1),1.]) .: N
by A46;
then
m in N1
by A44;
hence
m in V
by A37;
verum
end; hence
Circle2IntervalL is_continuous_at p
by TMAP_1:43;
verum
end;
hence
Circle2IntervalL is continuous
by TMAP_1:44; verum