reconsider D = NonZero (TOP-REAL 2) as non empty Subset of (TOP-REAL 2) by JGRAPH_2:9;
let sn be Real; ( - 1 < sn & sn < 1 implies ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphE & h is continuous ) )
assume that
A1:
- 1 < sn
and
A2:
sn < 1
; 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) ;
A3:
f . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)
by Th82, JGRAPH_2:3;
A4:
for p being Point of ((TOP-REAL 2) | D) holds f . p <> f . (0. (TOP-REAL 2))
A15:
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
reconsider u0 =
0. (TOP-REAL 2) as
Point of
(Euclid 2) by EUCLID:67;
let V be
Subset of
(TOP-REAL 2);
( 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 ) )
reconsider VV =
V as
Subset of
(TopSpaceMetr (Euclid 2)) by Lm11;
assume that A16:
f . (0. (TOP-REAL 2)) in V
and A17:
V is
open
;
ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V )
VV is
open
by A17, Lm11, PRE_TOPC:30;
then consider r being
Real such that A18:
r > 0
and A19:
Ball (
u0,
r)
c= V
by A3, A16, TOPMETR:15;
reconsider r =
r as
Real ;
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) ;
A20:
W1 is
open
by GOBOARD6:3;
A21:
f .: W1 c= W1
proof
let z be
object ;
TARSKI:def 3 ( not z in f .: W1 or z in W1 )
assume
z in f .: W1
;
z in W1
then consider y being
object such that A22:
y in dom f
and A23:
y in W1
and A24:
z = f . y
by FUNCT_1:def 6;
z in rng f
by A22, A24, FUNCT_1:def 3;
then reconsider qz =
z as
Point of
(TOP-REAL 2) ;
reconsider q =
y as
Point of
(TOP-REAL 2) by A22;
reconsider qy =
q as
Point of
(Euclid 2) by EUCLID:67;
reconsider pz =
qz as
Point of
(Euclid 2) by EUCLID:67;
dist (
u0,
qy)
< r
by A23, METRIC_1:11;
then A25:
|.((0. (TOP-REAL 2)) - q).| < r
by JGRAPH_1:28;
now ( ( q `1 <= 0 & z in W1 ) or ( q <> 0. (TOP-REAL 2) & (q `2) / |.q.| >= sn & q `1 >= 0 & z in W1 ) or ( q <> 0. (TOP-REAL 2) & (q `2) / |.q.| < sn & q `1 >= 0 & z in W1 ) )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:3;
case A26:
(
q <> 0. (TOP-REAL 2) &
(q `2) / |.q.| >= sn &
q `1 >= 0 )
;
z in W1then A27:
((q `2) / |.q.|) - sn >= 0
by XREAL_1:48;
0 <= (q `1) ^2
by XREAL_1:63;
then
(
|.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) &
0 + ((q `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then A28:
((q `2) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2)
by XREAL_1:72;
A29:
1
- sn > 0
by A2, XREAL_1:149;
|.q.| <> 0
by A26, TOPRNS_1:24;
then
|.q.| ^2 > 0
by SQUARE_1:12;
then
((q `2) ^2) / (|.q.| ^2) <= 1
by A28, XCMPLX_1:60;
then
((q `2) / |.q.|) ^2 <= 1
by XCMPLX_1:76;
then
1
>= (q `2) / |.q.|
by SQUARE_1:51;
then
1
- sn >= ((q `2) / |.q.|) - sn
by XREAL_1:9;
then
- (1 - sn) <= - (((q `2) / |.q.|) - sn)
by XREAL_1:24;
then
(- (1 - sn)) / (1 - sn) <= (- (((q `2) / |.q.|) - sn)) / (1 - sn)
by A29, XREAL_1:72;
then
- 1
<= (- (((q `2) / |.q.|) - sn)) / (1 - sn)
by A29, XCMPLX_1:197;
then
((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2 <= 1
^2
by A29, A27, SQUARE_1:49;
then
1
- (((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2) >= 0
by XREAL_1:48;
then A30:
1
- ((- ((((q `2) / |.q.|) - sn) / (1 - sn))) ^2) >= 0
by XCMPLX_1:187;
A31:
(sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]|
by A1, A2, A26, Th84;
then A32:
qz `2 = |.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn))
by A24, EUCLID:52;
qz `1 = |.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))
by A24, A31, EUCLID:52;
then A33:
(qz `1) ^2 =
(|.q.| ^2) * ((sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))) ^2)
.=
(|.q.| ^2) * (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))
by A30, SQUARE_1:def 2
;
|.qz.| ^2 =
((qz `1) ^2) + ((qz `2) ^2)
by JGRAPH_3:1
.=
|.q.| ^2
by A32, A33
;
then
sqrt (|.qz.| ^2) = |.q.|
by SQUARE_1:22;
then A34:
|.qz.| = |.q.|
by SQUARE_1:22;
|.(- q).| < r
by A25, RLVECT_1:4;
then
|.q.| < r
by TOPRNS_1:26;
then
|.(- qz).| < r
by A34, TOPRNS_1:26;
then
|.((0. (TOP-REAL 2)) - qz).| < r
by RLVECT_1:4;
then
dist (
u0,
pz)
< r
by JGRAPH_1:28;
hence
z in W1
by METRIC_1:11;
verum end; case A35:
(
q <> 0. (TOP-REAL 2) &
(q `2) / |.q.| < sn &
q `1 >= 0 )
;
z in W1
0 <= (q `1) ^2
by XREAL_1:63;
then
(
|.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) &
0 + ((q `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then A36:
((q `2) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2)
by XREAL_1:72;
A37:
1
+ sn > 0
by A1, XREAL_1:148;
|.q.| <> 0
by A35, TOPRNS_1:24;
then
|.q.| ^2 > 0
by SQUARE_1:12;
then
((q `2) ^2) / (|.q.| ^2) <= 1
by A36, XCMPLX_1:60;
then
((q `2) / |.q.|) ^2 <= 1
by XCMPLX_1:76;
then
- 1
<= (q `2) / |.q.|
by SQUARE_1:51;
then
- (- 1) >= - ((q `2) / |.q.|)
by XREAL_1:24;
then
1
+ sn >= (- ((q `2) / |.q.|)) + sn
by XREAL_1:7;
then A38:
(- (((q `2) / |.q.|) - sn)) / (1 + sn) <= 1
by A37, XREAL_1:185;
sn - ((q `2) / |.q.|) >= 0
by A35, XREAL_1:48;
then
- 1
<= (- (((q `2) / |.q.|) - sn)) / (1 + sn)
by A37;
then
((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2 <= 1
^2
by A38, SQUARE_1:49;
then
1
- (((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2) >= 0
by XREAL_1:48;
then A39:
1
- ((- ((((q `2) / |.q.|) - sn) / (1 + sn))) ^2) >= 0
by XCMPLX_1:187;
A40:
(sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]|
by A1, A2, A35, Th84;
then A41:
qz `2 = |.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn))
by A24, EUCLID:52;
qz `1 = |.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))
by A24, A40, EUCLID:52;
then A42:
(qz `1) ^2 =
(|.q.| ^2) * ((sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))) ^2)
.=
(|.q.| ^2) * (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))
by A39, SQUARE_1:def 2
;
|.qz.| ^2 =
((qz `1) ^2) + ((qz `2) ^2)
by JGRAPH_3:1
.=
|.q.| ^2
by A41, A42
;
then
sqrt (|.qz.| ^2) = |.q.|
by SQUARE_1:22;
then A43:
|.qz.| = |.q.|
by SQUARE_1:22;
|.(- q).| < r
by A25, RLVECT_1:4;
then
|.q.| < r
by TOPRNS_1:26;
then
|.(- qz).| < r
by A43, TOPRNS_1:26;
then
|.((0. (TOP-REAL 2)) - qz).| < r
by RLVECT_1:4;
then
dist (
u0,
pz)
< r
by JGRAPH_1:28;
hence
z in W1
by METRIC_1:11;
verum end; end; end;
hence
z in W1
;
verum
end;
u0 in W1
by A18, GOBOARD6:1;
hence
ex
W being
Subset of
(TOP-REAL 2) st
(
0. (TOP-REAL 2) in W &
W is
open &
f .: W c= V )
by A19, A20, A21, XBOOLE_1:1;
verum
end;
A44:
D ` = {(0. (TOP-REAL 2))}
by JGRAPH_3:20;
then
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphE) | D & h is continuous )
by A1, A2, Th100;
hence
ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphE & h is continuous )
by A3, A44, A4, A15, JGRAPH_3:3; verum