reconsider l = AffineMap ((2 * PI),0) as Function of R^1,R^1 by Th8;
set sR = R^1 sin;
set cR = R^1 cos;
A1:
dom (AffineMap ((2 * PI),0)) = REAL
by FUNCT_2:def 1;
reconsider sR = R^1 sin, cR = R^1 cos as Function of R^1,R^1 by Lm10, Lm11;
A2:
AffineMap ((2 * PI),0) = R^1 (AffineMap ((2 * PI),0))
;
reconsider g = CircleMap as Function of R^1,(TOP-REAL 2) by TOPREALA:7;
A3:
rng (AffineMap ((2 * PI),0)) = [#] REAL
by FCONT_1:55;
set c = cR * l;
set s = sR * l;
A4:
R^1 | (R^1 (dom cos)) = R^1
by Th6, SIN_COS:24;
A5:
R^1 | (R^1 (dom sin)) = R^1
by Th6, SIN_COS:24;
for p being Point of R^1
for V being Subset of (TOP-REAL 2) st g . p in V & V is open holds
ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )
proof
let p be
Point of
R^1;
for V being Subset of (TOP-REAL 2) st g . p in V & V is open holds
ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )let V be
Subset of
(TOP-REAL 2);
( g . p in V & V is open implies ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V ) )
assume that A6:
g . p in V
and A7:
V is
open
;
ex W being Subset of R^1 st
( p in W & W is open & g .: W c= V )
reconsider e =
g . p as
Point of
(Euclid 2) by TOPREAL3:8;
V = Int V
by A7, TOPS_1:23;
then consider r being
Real such that A8:
r > 0
and A9:
Ball (
e,
r)
c= V
by A6, GOBOARD6:5;
set B =
].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[;
set A =
].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[;
set F = (1,2)
--> (
].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,
].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[);
reconsider A =
].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,
B =
].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[ as
Subset of
R^1 by TOPMETR:17;
A10:
B is
open
by JORDAN6:35;
A11:
product ((1,2) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[)) c= Ball (
e,
r)
by TOPREAL6:41;
A12:
cR is
continuous
by A4, PRE_TOPC:26;
A13:
sR is
continuous
by A5, PRE_TOPC:26;
A14:
g . p = |[((cR * l) . p),((sR * l) . p)]|
by Lm20;
then
(g . p) `2 = (sR * l) . p
by EUCLID:52;
then
(sR * l) . p in B
by A8, SQUARE_1:19, TOPREAL6:15;
then consider Ws being
Subset of
R^1 such that A15:
p in Ws
and A16:
Ws is
open
and A17:
(sR * l) .: Ws c= B
by A2, A1, A3, A10, A13, Th5, JGRAPH_2:10;
A18:
A is
open
by JORDAN6:35;
(g . p) `1 = (cR * l) . p
by A14, EUCLID:52;
then
(cR * l) . p in A
by A8, SQUARE_1:19, TOPREAL6:15;
then consider Wc being
Subset of
R^1 such that A19:
p in Wc
and A20:
Wc is
open
and A21:
(cR * l) .: Wc c= A
by A2, A1, A3, A18, A12, Th5, JGRAPH_2:10;
set W =
Ws /\ Wc;
take
Ws /\ Wc
;
( p in Ws /\ Wc & Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus
p in Ws /\ Wc
by A15, A19, XBOOLE_0:def 4;
( Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus
Ws /\ Wc is
open
by A16, A20;
g .: (Ws /\ Wc) c= V
let y be
object ;
TARSKI:def 3 ( not y in g .: (Ws /\ Wc) or y in V )
assume
y in g .: (Ws /\ Wc)
;
y in V
then consider x being
Element of
R^1 such that A22:
x in Ws /\ Wc
and A23:
y = g . x
by FUNCT_2:65;
x in Ws
by A22, XBOOLE_0:def 4;
then A24:
(sR * l) . x in (sR * l) .: Ws
by FUNCT_2:35;
x in Wc
by A22, XBOOLE_0:def 4;
then A25:
(cR * l) . x in (cR * l) .: Wc
by FUNCT_2:35;
|[((cR * l) . x),((sR * l) . x)]| = (1,2)
--> (
((cR * l) . x),
((sR * l) . x))
by TOPREALA:28;
then
|[((cR * l) . x),((sR * l) . x)]| in product ((1,2) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[))
by A17, A21, A24, A25, HILBERT3:11;
then A26:
|[((cR * l) . x),((sR * l) . x)]| in Ball (
e,
r)
by A11;
g . x = |[((cR * l) . x),((sR * l) . x)]|
by Lm20;
hence
y in V
by A9, A23, A26;
verum
end;
then
g is continuous
by JGRAPH_2:10;
hence
CircleMap is continuous
by PRE_TOPC:27; verum