A1:
AffineMap ((2 * PI),0) = R^1 (AffineMap ((2 * PI),0))
;
A2:
R^1 | (R^1 (dom sin)) = R^1
by SIN_COS:24, TOPREALB:6;
A3:
R^1 | (R^1 (dom cos)) = R^1
by SIN_COS:24, TOPREALB:6;
set sR = R^1 sin;
set cR = R^1 cos;
reconsider sR = R^1 sin, cR = R^1 cos as Function of R^1,R^1 by Lm10, Lm11;
reconsider l = AffineMap ((2 * PI),0) as Function of R^1,R^1 by TOPREALB:8;
A4:
dom (AffineMap ((2 * PI),0)) = REAL
by FUNCT_2:def 1;
A5:
rng (AffineMap ((2 * PI),0)) = [#] REAL
by FCONT_1:55;
set s = sR * l;
set c = cR * l;
reconsider g = SphereMap as Function of R^1,(TOP-REAL 3) by TOPREALA:7;
for p being Point of R^1
for V being Subset of (TOP-REAL 3) 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 3) 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 3);
( 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 )
A8:
V = Int V
by A7, TOPS_1:23;
reconsider e =
g . p as
Point of
(Euclid 3) by TOPREAL3:8;
consider r being
Real such that A9:
r > 0
and A10:
Ball (
e,
r)
c= V
by A6, A8, GOBOARD6:5;
set A =
].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[;
set B =
].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[;
set F = (1,2,3)
--> (
].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,
].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,
{0});
A11:
g . p = |[((cR * l) . p),((sR * l) . p),0]|
by Lm12;
then A12:
(g . p) `2 = (sR * l) . p
by EUCLID_5:2;
(g . p) `3 = 0
by A11, EUCLID_5:2;
then A13:
product ((1,2,3) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,{0})) c= Ball (
e,
r)
by Th38;
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;
A14:
A is
open
by JORDAN6:35;
A15:
B is
open
by JORDAN6:35;
A16:
sR is
continuous
by A2, PRE_TOPC:26;
(sR * l) . p in B
by A9, A12, TOPREAL6:15;
then consider Ws being
Subset of
R^1 such that A17:
p in Ws
and A18:
Ws is
open
and A19:
(sR * l) .: Ws c= B
by A15, A16, A1, A4, A5, JGRAPH_2:10, TOPREALB:5;
A20:
(g . p) `1 = (cR * l) . p
by A11, EUCLID_5:2;
A21:
cR is
continuous
by A3, PRE_TOPC:26;
(cR * l) . p in A
by A9, A20, TOPREAL6:15;
then consider Wc being
Subset of
R^1 such that A22:
p in Wc
and A23:
Wc is
open
and A24:
(cR * l) .: Wc c= A
by A14, A21, A1, A4, A5, JGRAPH_2:10, TOPREALB:5;
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 A17, A22, XBOOLE_0:def 4;
( Ws /\ Wc is open & g .: (Ws /\ Wc) c= V )
thus
Ws /\ Wc is
open
by A18, A23;
g .: (Ws /\ Wc) c= V
let y be
Point of
(TOP-REAL 3);
LATTICE7:def 1 ( 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 A25:
x in Ws /\ Wc
and A26:
y = g . x
by FUNCT_2:65;
A27:
g . x = |[((cR * l) . x),((sR * l) . x),0]|
by Lm12;
x in Ws
by A25, XBOOLE_0:def 4;
then A28:
(sR * l) . x in (sR * l) .: Ws
by FUNCT_2:35;
x in Wc
by A25, XBOOLE_0:def 4;
then A29:
(cR * l) . x in (cR * l) .: Wc
by FUNCT_2:35;
|[((cR * l) . x),((sR * l) . x),0]| = (1,2,3)
--> (
((cR * l) . x),
((sR * l) . x),
0)
by Th20;
then
|[((cR * l) . x),((sR * l) . x),0]| in product ((1,2,3) --> (].(((g . p) `1) - (r / (sqrt 2))),(((g . p) `1) + (r / (sqrt 2))).[,].(((g . p) `2) - (r / (sqrt 2))),(((g . p) `2) + (r / (sqrt 2))).[,{0}))
by A19, A24, A28, A29, Lm2, Lm6, Th23;
then
|[((cR * l) . x),((sR * l) . x),0]| in Ball (
e,
r)
by A13;
hence
y in V
by A10, A26, A27;
verum
end;
then
g is continuous
by JGRAPH_2:10;
hence
SphereMap is continuous
by PRE_TOPC:27; verum