reconsider f = Sq_Circ " as Function of (TOP-REAL 2),(TOP-REAL 2) by Th39;
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 Th38;
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))
A18:
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (Sq_Circ " ) | D & h is continuous )
by A2, Th51;
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 A19:
(
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 A19, PRE_TOPC:60, TT;
then consider r being
real number such that A20:
(
r > 0 &
Ball u0,
r c= V )
by A1, A19, TOPMETR:22, TT;
reconsider r =
r as
Real by XREAL_0:def 1;
sqrt 2
> 0
by SQUARE_1:93;
then A21:
r / (sqrt 2) > 0
by A20, XREAL_1:141;
reconsider W1 =
Ball u0,
r,
V1 =
Ball u0,
(r / (sqrt 2)) as
Subset of
(TOP-REAL 2) by VV;
A22:
u0 in V1
by A21, GOBOARD6:4;
A23:
V1 is
open
by GOBOARD6:6;
f .: V1 c= W1
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in f .: V1 or z in W1 )
assume
z in f .: V1
;
:: thesis: z in W1
then consider y being
set such that A24:
(
y in dom f &
y in V1 &
z = f . y )
by FUNCT_1:def 12;
reconsider q =
y as
Point of
(TOP-REAL 2) by A24;
reconsider qy =
q as
Point of
(Euclid 2) by VV;
z in rng f
by A24, 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 / (sqrt 2)
by A24, METRIC_1:12;
then
|.((0. (TOP-REAL 2)) - q).| < r / (sqrt 2)
by JGRAPH_1:45;
then
sqrt (((((0. (TOP-REAL 2)) - q) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - q) `2 ) ^2 )) < r / (sqrt 2)
by JGRAPH_1:47;
then
sqrt (((((0. (TOP-REAL 2)) `1 ) - (q `1 )) ^2 ) + ((((0. (TOP-REAL 2)) - q) `2 ) ^2 )) < r / (sqrt 2)
by TOPREAL3:8;
then A25:
sqrt (((((0. (TOP-REAL 2)) `1 ) - (q `1 )) ^2 ) + ((((0. (TOP-REAL 2)) `2 ) - (q `2 )) ^2 )) < r / (sqrt 2)
by TOPREAL3:8;
A26:
(q `1 ) ^2 >= 0
by XREAL_1:65;
A27:
(q `2 ) ^2 >= 0
by XREAL_1:65;
then A28:
((q `1 ) ^2 ) + ((q `2 ) ^2 ) >= 0 + 0
by A26;
A29:
sqrt 2
> 0
by SQUARE_1:93;
then
(sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 ))) * (sqrt 2) < (r / (sqrt 2)) * (sqrt 2)
by A25, JGRAPH_2:11, XREAL_1:70;
then
sqrt ((((q `1 ) ^2 ) + ((q `2 ) ^2 )) * 2) < (r / (sqrt 2)) * (sqrt 2)
by A28, SQUARE_1:97;
then A30:
sqrt ((((q `1 ) ^2 ) + ((q `2 ) ^2 )) * 2) < r
by A29, XCMPLX_1:88;
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 A31:
(
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 A32:
(Sq_Circ " ) . q = |[((q `1 ) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]|
by Th38;
A33:
((0. (TOP-REAL 2)) - qz) `1 =
((0. (TOP-REAL 2)) `1 ) - (qz `1 )
by TOPREAL3:8
.=
- (qz `1 )
by JGRAPH_2:11
;
A34:
((0. (TOP-REAL 2)) - qz) `2 =
((0. (TOP-REAL 2)) `2 ) - (qz `2 )
by TOPREAL3:8
.=
- (qz `2 )
by JGRAPH_2:11
;
A35:
(
qz `1 = (q `1 ) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) &
qz `2 = (q `2 ) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) )
by A24, A32, EUCLID:56;
then
((q `2 ) ^2 ) / ((q `1 ) ^2 ) <= ((q `1 ) ^2 ) / ((q `1 ) ^2 )
by A36, XREAL_1:74;
then
((q `2 ) / (q `1 )) ^2 <= ((q `1 ) ^2 ) / ((q `1 ) ^2 )
by XCMPLX_1:77;
then
((q `2 ) / (q `1 )) ^2 <= 1
by A42, XCMPLX_1:60;
then A44:
1
+ (((q `2 ) / (q `1 )) ^2 ) <= 1
+ 1
by XREAL_1:9;
then A45:
((q `1 ) ^2 ) * (1 + (((q `2 ) / (q `1 )) ^2 )) <= ((q `1 ) ^2 ) * 2
by A26, XREAL_1:66;
A46:
((q `2 ) ^2 ) * (1 + (((q `2 ) / (q `1 )) ^2 )) <= ((q `2 ) ^2 ) * 2
by A27, A44, XREAL_1:66;
A47:
1
+ (((q `2 ) / (q `1 )) ^2 ) > 0
by Lm1;
(qz `1 ) ^2 = ((q `1 ) ^2 ) * ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )
by A35;
then A48:
(qz `1 ) ^2 <= ((q `1 ) ^2 ) * 2
by A45, A47, SQUARE_1:def 4;
A49:
(qz `1 ) ^2 >= 0
by XREAL_1:65;
A50:
(qz `2 ) ^2 = ((q `2 ) ^2 ) * ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )
by A35;
A51:
(qz `2 ) ^2 >= 0
by XREAL_1:65;
(qz `2 ) ^2 <= ((q `2 ) ^2 ) * 2
by A46, A47, A50, SQUARE_1:def 4;
then A52:
((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) <= (((q `1 ) ^2 ) * 2) + (((q `2 ) ^2 ) * 2)
by A48, XREAL_1:9;
0 + 0 <= ((qz `1 ) ^2 ) + ((qz `2 ) ^2 )
by A49, A51;
then
sqrt (((qz `1 ) ^2 ) + ((qz `2 ) ^2 )) <= sqrt ((((q `1 ) ^2 ) * 2) + (((q `2 ) ^2 ) * 2))
by A52, SQUARE_1:94;
then
sqrt (((((0. (TOP-REAL 2)) - qz) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - qz) `2 ) ^2 )) < r
by A30, A33, A34, 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 A53:
(
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 A54:
(Sq_Circ " ) . q = |[((q `1 ) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]|
by Th38;
A55:
((0. (TOP-REAL 2)) - qz) `1 =
((0. (TOP-REAL 2)) `1 ) - (qz `1 )
by TOPREAL3:8
.=
- (qz `1 )
by JGRAPH_2:11
;
A56:
((0. (TOP-REAL 2)) - qz) `2 =
((0. (TOP-REAL 2)) `2 ) - (qz `2 )
by TOPREAL3:8
.=
- (qz `2 )
by JGRAPH_2:11
;
A57:
(
qz `1 = (q `1 ) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) &
qz `2 = (q `2 ) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) )
by A24, A54, EUCLID:56;
then
((q `1 ) ^2 ) / ((q `2 ) ^2 ) <= ((q `2 ) ^2 ) / ((q `2 ) ^2 )
by A59, XREAL_1:74;
then
((q `1 ) / (q `2 )) ^2 <= ((q `2 ) ^2 ) / ((q `2 ) ^2 )
by XCMPLX_1:77;
then
((q `1 ) / (q `2 )) ^2 <= 1
by A65, XCMPLX_1:60;
then A66:
1
+ (((q `1 ) / (q `2 )) ^2 ) <= 1
+ 1
by XREAL_1:9;
then A67:
((q `2 ) ^2 ) * (1 + (((q `1 ) / (q `2 )) ^2 )) <= ((q `2 ) ^2 ) * 2
by A27, XREAL_1:66;
A68:
((q `1 ) ^2 ) * (1 + (((q `1 ) / (q `2 )) ^2 )) <= ((q `1 ) ^2 ) * 2
by A26, A66, XREAL_1:66;
1
+ (((q `1 ) / (q `2 )) ^2 ) > 0
by Lm1;
then A69:
(sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 = 1
+ (((q `1 ) / (q `2 )) ^2 )
by SQUARE_1:def 4;
then A70:
(qz `2 ) ^2 <= ((q `2 ) ^2 ) * 2
by A57, A67, SQUARE_1:68;
A71:
(qz `2 ) ^2 >= 0
by XREAL_1:65;
A72:
(qz `1 ) ^2 >= 0
by XREAL_1:65;
(qz `1 ) ^2 <= ((q `1 ) ^2 ) * 2
by A57, A68, A69, SQUARE_1:68;
then A73:
((qz `2 ) ^2 ) + ((qz `1 ) ^2 ) <= (((q `2 ) ^2 ) * 2) + (((q `1 ) ^2 ) * 2)
by A70, XREAL_1:9;
0 + 0 <= ((qz `2 ) ^2 ) + ((qz `1 ) ^2 )
by A71, A72;
then
sqrt (((qz `2 ) ^2 ) + ((qz `1 ) ^2 )) <= sqrt ((((q `2 ) ^2 ) * 2) + (((q `1 ) ^2 ) * 2))
by A73, SQUARE_1:94;
then
sqrt (((((0. (TOP-REAL 2)) - qz) `2 ) ^2 ) + ((((0. (TOP-REAL 2)) - qz) `1 ) ^2 )) < r
by A30, A55, A56, 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 A20, A22, A23, XBOOLE_1:1;
:: thesis: verum
end;
then
f is continuous
by A1, A2, A3, A18, Th13;
hence
ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = Sq_Circ " & h is continuous )
; :: thesis: verum