let sn be Real; :: thesis: ( - 1 < sn & sn < 1 implies ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphE & h is continuous ) )
assume A1:
( - 1 < sn & sn < 1 )
; :: thesis: ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphE & h is continuous )
reconsider f = sn -FanMorphE as Function of (TOP-REAL 2),(TOP-REAL 2) ;
reconsider D = NonZero (TOP-REAL 2) as non empty Subset of (TOP-REAL 2) by JGRAPH_2:19;
A2:
f . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)
by Th89, JGRAPH_2:11;
A3:
D ` = {(0. (TOP-REAL 2))}
by JGRAPH_3:30;
A4:
for p being Point of ((TOP-REAL 2) | D) holds f . p <> f . (0. (TOP-REAL 2))
A16:
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphE ) | D & h is continuous )
by A1, A3, Th107;
for V being Subset of (TOP-REAL 2) st f . (0. (TOP-REAL 2)) in V & V is open holds
ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V )
proof
let V be
Subset of
(TOP-REAL 2);
:: thesis: ( f . (0. (TOP-REAL 2)) in V & V is open implies ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V ) )
assume A17:
(
f . (0. (TOP-REAL 2)) in V &
V is
open )
;
:: thesis: ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V )
reconsider u0 =
0. (TOP-REAL 2) as
Point of
(Euclid 2) by EUCLID:71;
reconsider VV =
V as
Subset of
(TopSpaceMetr (Euclid 2)) by XX;
VV is
open
by A17, XX, PRE_TOPC:60;
then consider r being
real number such that A18:
(
r > 0 &
Ball u0,
r c= V )
by A2, A17, TOPMETR:22;
reconsider r =
r as
Real by XREAL_0:def 1;
TopStruct(# the
carrier of
(TOP-REAL 2),the
topology of
(TOP-REAL 2) #)
= TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
then reconsider W1 =
Ball u0,
r as
Subset of
(TOP-REAL 2) ;
A19:
u0 in W1
by A18, GOBOARD6:4;
A20:
W1 is
open
by GOBOARD6:6;
f .: W1 c= W1
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in f .: W1 or z in W1 )
assume
z in f .: W1
;
:: thesis: z in W1
then consider y being
set such that A21:
(
y in dom f &
y in W1 &
z = f . y )
by FUNCT_1:def 12;
reconsider q =
y as
Point of
(TOP-REAL 2) by A21;
reconsider qy =
q as
Point of
(Euclid 2) by EUCLID:71;
z in rng f
by A21, FUNCT_1:def 5;
then reconsider qz =
z as
Point of
(TOP-REAL 2) ;
reconsider pz =
qz as
Point of
(Euclid 2) by EUCLID:71;
dist u0,
qy < r
by A21, METRIC_1:12;
then A22:
|.((0. (TOP-REAL 2)) - q).| < r
by JGRAPH_1:45;
now per cases
( q `1 <= 0 or ( q <> 0. (TOP-REAL 2) & (q `2 ) / |.q.| >= sn & q `1 >= 0 ) or ( q <> 0. (TOP-REAL 2) & (q `2 ) / |.q.| < sn & q `1 >= 0 ) )
by JGRAPH_2:11;
case A23:
(
q <> 0. (TOP-REAL 2) &
(q `2 ) / |.q.| >= sn &
q `1 >= 0 )
;
:: thesis: z in W1then A24:
(sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]|
by A1, Th91;
|.q.| <> 0
by A23, TOPRNS_1:25;
then A25:
|.q.| ^2 > 0
by SQUARE_1:74;
A26:
1
- sn > 0
by A1, XREAL_1:151;
A27:
(
qz `1 = |.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))) &
qz `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)) )
by A21, A24, EUCLID:56;
A28:
((q `2 ) / |.q.|) - sn >= 0
by A23, XREAL_1:50;
A29:
|.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 )
by JGRAPH_3:10;
0 <= (q `1 ) ^2
by XREAL_1:65;
then
0 + ((q `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 )
by XREAL_1:9;
then
((q `2 ) ^2 ) / (|.q.| ^2 ) <= (|.q.| ^2 ) / (|.q.| ^2 )
by A29, XREAL_1:74;
then
((q `2 ) ^2 ) / (|.q.| ^2 ) <= 1
by A25, XCMPLX_1:60;
then
((q `2 ) / |.q.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (q `2 ) / |.q.|
by SQUARE_1:121;
then A30:
1
- sn >= ((q `2 ) / |.q.|) - sn
by XREAL_1:11;
A31:
- (1 - sn) <= - 0
by A26;
- (1 - sn) <= - (((q `2 ) / |.q.|) - sn)
by A30, XREAL_1:26;
then
(- (1 - sn)) / (1 - sn) <= (- (((q `2 ) / |.q.|) - sn)) / (1 - sn)
by A26, XREAL_1:74;
then A32:
- 1
<= (- (((q `2 ) / |.q.|) - sn)) / (1 - sn)
by A26, XCMPLX_1:198;
- (- (1 - sn)) >= - (((q `2 ) / |.q.|) - sn)
by A28, A31, XREAL_1:26;
then
(- (((q `2 ) / |.q.|) - sn)) / (1 - sn) <= 1
by A26, XREAL_1:187;
then
((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 <= 1
^2
by A32, SQUARE_1:119;
then
1
- (((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 ) >= 0
by XREAL_1:50;
then A33:
1
- ((- ((((q `2 ) / |.q.|) - sn) / (1 - sn))) ^2 ) >= 0
by XCMPLX_1:188;
A34:
(qz `1 ) ^2 =
(|.q.| ^2 ) * ((sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))) ^2 )
by A27
.=
(|.q.| ^2 ) * (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))
by A33, SQUARE_1:def 4
;
|.qz.| ^2 =
((qz `1 ) ^2 ) + ((qz `2 ) ^2 )
by JGRAPH_3:10
.=
|.q.| ^2
by A27, A34
;
then
sqrt (|.qz.| ^2 ) = |.q.|
by SQUARE_1:89;
then A35:
|.qz.| = |.q.|
by SQUARE_1:89;
|.((0. (TOP-REAL 2)) + (- q)).| < r
by A22, EUCLID:45;
then
|.(- q).| < r
by EUCLID:31;
then
|.q.| < r
by TOPRNS_1:27;
then
|.(- qz).| < r
by A35, TOPRNS_1:27;
then
|.((0. (TOP-REAL 2)) + (- qz)).| < r
by EUCLID:31;
then
|.((0. (TOP-REAL 2)) - qz).| < r
by EUCLID:45;
then
dist u0,
pz < r
by JGRAPH_1:45;
hence
z in W1
by METRIC_1:12;
:: thesis: verum end; case A36:
(
q <> 0. (TOP-REAL 2) &
(q `2 ) / |.q.| < sn &
q `1 >= 0 )
;
:: thesis: z in W1then A37:
(sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]|
by A1, Th91;
|.q.| <> 0
by A36, TOPRNS_1:25;
then A38:
|.q.| ^2 > 0
by SQUARE_1:74;
A39:
sn - ((q `2 ) / |.q.|) >= 0
by A36, XREAL_1:50;
A40:
|.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 )
by JGRAPH_3:10;
A41:
1
+ sn > 0
by A1, XREAL_1:150;
A42:
(
qz `1 = |.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))) &
qz `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)) )
by A21, A37, EUCLID:56;
0 <= (q `1 ) ^2
by XREAL_1:65;
then
0 + ((q `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 )
by XREAL_1:9;
then
((q `2 ) ^2 ) / (|.q.| ^2 ) <= (|.q.| ^2 ) / (|.q.| ^2 )
by A40, XREAL_1:74;
then
((q `2 ) ^2 ) / (|.q.| ^2 ) <= 1
by A38, XCMPLX_1:60;
then
((q `2 ) / |.q.|) ^2 <= 1
by XCMPLX_1:77;
then
- 1
<= (q `2 ) / |.q.|
by SQUARE_1:121;
then
- (- 1) >= - ((q `2 ) / |.q.|)
by XREAL_1:26;
then A43:
1
+ sn >= (- ((q `2 ) / |.q.|)) + sn
by XREAL_1:9;
(- (1 + sn)) / (1 + sn) <= (- (((q `2 ) / |.q.|) - sn)) / (1 + sn)
by A39, A41, XREAL_1:74;
then A44:
- 1
<= (- (((q `2 ) / |.q.|) - sn)) / (1 + sn)
by A41, XCMPLX_1:198;
(- (((q `2 ) / |.q.|) - sn)) / (1 + sn) <= 1
by A41, A43, XREAL_1:187;
then
((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 <= 1
^2
by A44, SQUARE_1:119;
then
1
- (((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 ) >= 0
by XREAL_1:50;
then A45:
1
- ((- ((((q `2 ) / |.q.|) - sn) / (1 + sn))) ^2 ) >= 0
by XCMPLX_1:188;
A46:
(qz `1 ) ^2 =
(|.q.| ^2 ) * ((sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))) ^2 )
by A42
.=
(|.q.| ^2 ) * (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))
by A45, SQUARE_1:def 4
;
|.qz.| ^2 =
((qz `1 ) ^2 ) + ((qz `2 ) ^2 )
by JGRAPH_3:10
.=
|.q.| ^2
by A42, A46
;
then
sqrt (|.qz.| ^2 ) = |.q.|
by SQUARE_1:89;
then A47:
|.qz.| = |.q.|
by SQUARE_1:89;
|.((0. (TOP-REAL 2)) + (- q)).| < r
by A22, EUCLID:45;
then
|.(- q).| < r
by EUCLID:31;
then
|.q.| < r
by TOPRNS_1:27;
then
|.(- qz).| < r
by A47, TOPRNS_1:27;
then
|.((0. (TOP-REAL 2)) + (- qz)).| < r
by EUCLID:31;
then
|.((0. (TOP-REAL 2)) - qz).| < r
by EUCLID:45;
then
dist u0,
pz < r
by JGRAPH_1:45;
hence
z in W1
by METRIC_1:12;
:: thesis: verum end;
hence
z in W1
;
:: thesis: verum
end;
hence
ex
W being
Subset of
(TOP-REAL 2) st
(
0. (TOP-REAL 2) in W &
W is
open &
f .: W c= V )
by A18, A19, A20, XBOOLE_1:1;
:: thesis: verum
end;
then
f is continuous
by A2, A3, A4, A16, JGRAPH_3:13;
hence
ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphE & h is continuous )
; :: thesis: verum