reconsider f = Sq_Circ 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;
A1:
f . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)
by Def1;
A2:
D ` = {(0. (TOP-REAL 2))}
by Th30;
A3:
for p being Point of ((TOP-REAL 2) | D) holds f . p <> f . (0. (TOP-REAL 2))
A20:
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous )
by A2, Th29;
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 A21:
(
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 VV;
reconsider VV =
V as
Subset of
(TopSpaceMetr (Euclid 2)) by TT;
VV is
open
by A21, PRE_TOPC:60, TT;
then consider r being
real number such that A22:
(
r > 0 &
Ball u0,
r c= V )
by A1, A21, TOPMETR:22;
reconsider r =
r as
Real by XREAL_0:def 1;
reconsider W1 =
Ball u0,
r as
Subset of
(TOP-REAL 2) by VV;
A23:
u0 in W1
by A22, GOBOARD6:4;
A24:
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 A25:
(
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 A25;
reconsider qy =
q as
Point of
(Euclid 2) by VV;
z in rng f
by A25, FUNCT_1:def 5;
then reconsider qz =
z as
Point of
(TOP-REAL 2) ;
reconsider pz =
qz as
Point of
(Euclid 2) by VV;
dist u0,
qy < r
by A25, METRIC_1:12;
then
|.((0. (TOP-REAL 2)) - q).| < r
by JGRAPH_1:45;
then
sqrt (((((0. (TOP-REAL 2)) - q) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - q) `2 ) ^2 )) < r
by JGRAPH_1:47;
then
sqrt (((((0. (TOP-REAL 2)) `1 ) - (q `1 )) ^2 ) + ((((0. (TOP-REAL 2)) - q) `2 ) ^2 )) < r
by TOPREAL3:8;
then A26:
sqrt (((((0. (TOP-REAL 2)) `1 ) - (q `1 )) ^2 ) + ((((0. (TOP-REAL 2)) `2 ) - (q `2 )) ^2 )) < r
by TOPREAL3:8;
per cases
( q = 0. (TOP-REAL 2) or ( q <> 0. (TOP-REAL 2) & ( ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ) or ( q <> 0. (TOP-REAL 2) & not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) )
;
suppose
(
q <> 0. (TOP-REAL 2) & ( (
q `2 <= q `1 &
- (q `1 ) <= q `2 ) or (
q `2 >= q `1 &
q `2 <= - (q `1 ) ) ) )
;
:: thesis: z in W1then A27:
Sq_Circ . q = |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]|
by Def1;
A28:
((0. (TOP-REAL 2)) - qz) `1 =
((0. (TOP-REAL 2)) `1 ) - (qz `1 )
by TOPREAL3:8
.=
- (qz `1 )
by JGRAPH_2:11
;
A29:
((0. (TOP-REAL 2)) - qz) `2 =
((0. (TOP-REAL 2)) `2 ) - (qz `2 )
by TOPREAL3:8
.=
- (qz `2 )
by JGRAPH_2:11
;
((q `2 ) / (q `1 )) ^2 >= 0
by XREAL_1:65;
then
1
+ (((q `2 ) / (q `1 )) ^2 ) >= 1
+ 0
by XREAL_1:9;
then A30:
sqrt (1 + (((q `2 ) / (q `1 )) ^2 )) >= 1
by SQUARE_1:83, SQUARE_1:94;
then
(sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 >= sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))
by XREAL_1:153;
then A31:
1
<= (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2
by A30, XXREAL_0:2;
A32:
(qz `1 ) ^2 =
((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))) ^2
by A25, A27, EUCLID:56
.=
((q `1 ) ^2 ) / ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )
by XCMPLX_1:77
;
A33:
(qz `1 ) ^2 >= 0
by XREAL_1:65;
(q `1 ) ^2 >= 0
by XREAL_1:65;
then A34:
(qz `1 ) ^2 <= ((q `1 ) ^2 ) / 1
by A31, A32, XREAL_1:120;
A35:
(qz `2 ) ^2 =
((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))) ^2
by A25, A27, EUCLID:56
.=
((q `2 ) ^2 ) / ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )
by XCMPLX_1:77
;
A36:
(qz `2 ) ^2 >= 0
by XREAL_1:65;
(q `2 ) ^2 >= 0
by XREAL_1:65;
then
(qz `2 ) ^2 <= ((q `2 ) ^2 ) / 1
by A31, A35, XREAL_1:120;
then A37:
((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 )
by A34, XREAL_1:9;
0 + 0 <= ((qz `1 ) ^2 ) + ((qz `2 ) ^2 )
by A33, A36;
then
sqrt (((qz `1 ) ^2 ) + ((qz `2 ) ^2 )) <= sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 ))
by A37, SQUARE_1:94;
then
sqrt (((((0. (TOP-REAL 2)) - qz) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - qz) `2 ) ^2 )) < r
by A26, A28, A29, JGRAPH_2:11, XXREAL_0:2;
then
|.((0. (TOP-REAL 2)) - qz).| < r
by JGRAPH_1:47;
then
dist u0,
pz < r
by JGRAPH_1:45;
hence
z in W1
by METRIC_1:12;
:: thesis: verum end; suppose
(
q <> 0. (TOP-REAL 2) & not (
q `2 <= q `1 &
- (q `1 ) <= q `2 ) & not (
q `2 >= q `1 &
q `2 <= - (q `1 ) ) )
;
:: thesis: z in W1then A38:
Sq_Circ . q = |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]|
by Def1;
A39:
((0. (TOP-REAL 2)) - qz) `1 =
((0. (TOP-REAL 2)) `1 ) - (qz `1 )
by TOPREAL3:8
.=
- (qz `1 )
by JGRAPH_2:11
;
A40:
((0. (TOP-REAL 2)) - qz) `2 =
((0. (TOP-REAL 2)) `2 ) - (qz `2 )
by TOPREAL3:8
.=
- (qz `2 )
by JGRAPH_2:11
;
((q `1 ) / (q `2 )) ^2 >= 0
by XREAL_1:65;
then
1
+ (((q `1 ) / (q `2 )) ^2 ) >= 1
+ 0
by XREAL_1:9;
then A41:
sqrt (1 + (((q `1 ) / (q `2 )) ^2 )) >= 1
by SQUARE_1:83, SQUARE_1:94;
then
(sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 >= sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))
by XREAL_1:153;
then A42:
1
<= (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2
by A41, XXREAL_0:2;
A43:
(qz `1 ) ^2 =
((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))) ^2
by A25, A38, EUCLID:56
.=
((q `1 ) ^2 ) / ((sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 )
by XCMPLX_1:77
;
A44:
(qz `1 ) ^2 >= 0
by XREAL_1:65;
(q `1 ) ^2 >= 0
by XREAL_1:65;
then A45:
(qz `1 ) ^2 <= ((q `1 ) ^2 ) / 1
by A42, A43, XREAL_1:120;
A46:
(qz `2 ) ^2 =
((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))) ^2
by A25, A38, EUCLID:56
.=
((q `2 ) ^2 ) / ((sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 )
by XCMPLX_1:77
;
A47:
(qz `2 ) ^2 >= 0
by XREAL_1:65;
(q `2 ) ^2 >= 0
by XREAL_1:65;
then
(qz `2 ) ^2 <= ((q `2 ) ^2 ) / 1
by A42, A46, XREAL_1:120;
then A48:
((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 )
by A45, XREAL_1:9;
0 + 0 <= ((qz `1 ) ^2 ) + ((qz `2 ) ^2 )
by A44, A47;
then
sqrt (((qz `1 ) ^2 ) + ((qz `2 ) ^2 )) <= sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 ))
by A48, SQUARE_1:94;
then
sqrt (((((0. (TOP-REAL 2)) - qz) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - qz) `2 ) ^2 )) < r
by A26, A39, A40, JGRAPH_2:11, XXREAL_0:2;
then
|.((0. (TOP-REAL 2)) - qz).| < r
by JGRAPH_1:47;
then
dist u0,
pz < r
by JGRAPH_1:45;
hence
z in W1
by METRIC_1:12;
:: thesis: verum end;
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 A22, A23, A24, XBOOLE_1:1;
:: thesis: verum
end;
then
f is continuous
by A1, A2, A3, A20, Th13;
hence
ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = Sq_Circ & h is continuous )
; :: thesis: verum