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:
for p being Point of ((TOP-REAL 2) | D) holds f . p <> f . (0. (TOP-REAL 2))
A14:
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:71;
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 Lm16;
assume that A15:
f . (0. (TOP-REAL 2)) in V
and A16:
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 A16, Lm16, PRE_TOPC:60;
then consider r being
real number such that A17:
r > 0
and A18:
Ball u0,
r c= V
by A1, A15, TOPMETR:22;
reconsider r =
r as
Real by XREAL_0:def 1;
reconsider W1 =
Ball u0,
r,
V1 =
Ball u0,
(r / (sqrt 2)) as
Subset of
(TOP-REAL 2) by EUCLID:71;
A19:
f .: V1 c= W1
proof
let z be
set ;
TARSKI:def 3 ( not z in f .: V1 or z in W1 )
A20:
sqrt 2
> 0
by SQUARE_1:93;
assume
z in f .: V1
;
z in W1
then consider y being
set such that A21:
y in dom f
and A22:
y in V1
and A23:
z = f . y
by FUNCT_1:def 12;
z in rng f
by A21, A23, 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;
reconsider q =
y as
Point of
(TOP-REAL 2) by A21;
reconsider qy =
q as
Point of
(Euclid 2) by EUCLID:71;
A24:
(q `1 ) ^2 >= 0
by XREAL_1:65;
A25:
(q `2 ) ^2 >= 0
by XREAL_1:65;
dist u0,
qy < r / (sqrt 2)
by A22, 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
sqrt (((((0. (TOP-REAL 2)) `1 ) - (q `1 )) ^2 ) + ((((0. (TOP-REAL 2)) `2 ) - (q `2 )) ^2 )) < r / (sqrt 2)
by TOPREAL3:8;
then
(sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 ))) * (sqrt 2) < (r / (sqrt 2)) * (sqrt 2)
by A20, JGRAPH_2:11, XREAL_1:70;
then
sqrt ((((q `1 ) ^2 ) + ((q `2 ) ^2 )) * 2) < (r / (sqrt 2)) * (sqrt 2)
by A24, A25, SQUARE_1:97;
then A26:
sqrt ((((q `1 ) ^2 ) + ((q `2 ) ^2 )) * 2) < r
by A20, 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 A27:
(
q <> 0. (TOP-REAL 2) & ( (
q `2 <= q `1 &
- (q `1 ) <= q `2 ) or (
q `2 >= q `1 &
q `2 <= - (q `1 ) ) ) )
;
z in W1A30:
(Sq_Circ " ) . q = |[((q `1 ) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]|
by A27, Th38;
then
qz `1 = (q `1 ) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))
by A23, EUCLID:56;
then A31:
(qz `1 ) ^2 = ((q `1 ) ^2 ) * ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )
;
qz `2 = (q `2 ) * (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))
by A23, A30, EUCLID:56;
then A32:
(qz `2 ) ^2 = ((q `2 ) ^2 ) * ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )
;
A33:
1
+ (((q `2 ) / (q `1 )) ^2 ) > 0
by Lm1;
then
((q `2 ) ^2 ) / ((q `1 ) ^2 ) <= ((q `1 ) ^2 ) / ((q `1 ) ^2 )
by A28, 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 A28, XCMPLX_1:60;
then A38:
1
+ (((q `2 ) / (q `1 )) ^2 ) <= 1
+ 1
by XREAL_1:9;
then
((q `2 ) ^2 ) * (1 + (((q `2 ) / (q `1 )) ^2 )) <= ((q `2 ) ^2 ) * 2
by A25, XREAL_1:66;
then A39:
(qz `2 ) ^2 <= ((q `2 ) ^2 ) * 2
by A33, A32, SQUARE_1:def 4;
((q `1 ) ^2 ) * (1 + (((q `2 ) / (q `1 )) ^2 )) <= ((q `1 ) ^2 ) * 2
by A24, A38, XREAL_1:66;
then
(qz `1 ) ^2 <= ((q `1 ) ^2 ) * 2
by A33, A31, SQUARE_1:def 4;
then A40:
((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) <= (((q `1 ) ^2 ) * 2) + (((q `2 ) ^2 ) * 2)
by A39, XREAL_1:9;
(
(qz `1 ) ^2 >= 0 &
(qz `2 ) ^2 >= 0 )
by XREAL_1:65;
then A41:
sqrt (((qz `1 ) ^2 ) + ((qz `2 ) ^2 )) <= sqrt ((((q `1 ) ^2 ) * 2) + (((q `2 ) ^2 ) * 2))
by A40, SQUARE_1:94;
A42:
((0. (TOP-REAL 2)) - qz) `2 =
((0. (TOP-REAL 2)) `2 ) - (qz `2 )
by TOPREAL3:8
.=
- (qz `2 )
by JGRAPH_2:11
;
((0. (TOP-REAL 2)) - qz) `1 =
((0. (TOP-REAL 2)) `1 ) - (qz `1 )
by TOPREAL3:8
.=
- (qz `1 )
by JGRAPH_2:11
;
then
sqrt (((((0. (TOP-REAL 2)) - qz) `1 ) ^2 ) + ((((0. (TOP-REAL 2)) - qz) `2 ) ^2 )) < r
by A26, A42, A41, 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;
verum end; suppose A43:
(
q <> 0. (TOP-REAL 2) & not (
q `2 <= q `1 &
- (q `1 ) <= q `2 ) & not (
q `2 >= q `1 &
q `2 <= - (q `1 ) ) )
;
z in W1then
((q `1 ) ^2 ) / ((q `2 ) ^2 ) <= ((q `2 ) ^2 ) / ((q `2 ) ^2 )
by A44, 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 A44, XCMPLX_1:60;
then A49:
1
+ (((q `1 ) / (q `2 )) ^2 ) <= 1
+ 1
by XREAL_1:9;
then A50:
((q `2 ) ^2 ) * (1 + (((q `1 ) / (q `2 )) ^2 )) <= ((q `2 ) ^2 ) * 2
by A25, XREAL_1:66;
1
+ (((q `1 ) / (q `2 )) ^2 ) > 0
by Lm1;
then A51:
(sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 = 1
+ (((q `1 ) / (q `2 )) ^2 )
by SQUARE_1:def 4;
A52:
((q `1 ) ^2 ) * (1 + (((q `1 ) / (q `2 )) ^2 )) <= ((q `1 ) ^2 ) * 2
by A24, A49, XREAL_1:66;
A53:
(Sq_Circ " ) . q = |[((q `1 ) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]|
by A43, Th38;
then
qz `1 = (q `1 ) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))
by A23, EUCLID:56;
then A54:
(qz `1 ) ^2 <= ((q `1 ) ^2 ) * 2
by A52, A51, SQUARE_1:68;
qz `2 = (q `2 ) * (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))
by A23, A53, EUCLID:56;
then
(qz `2 ) ^2 <= ((q `2 ) ^2 ) * 2
by A50, A51, SQUARE_1:68;
then A55:
((qz `2 ) ^2 ) + ((qz `1 ) ^2 ) <= (((q `2 ) ^2 ) * 2) + (((q `1 ) ^2 ) * 2)
by A54, XREAL_1:9;
(
(qz `2 ) ^2 >= 0 &
(qz `1 ) ^2 >= 0 )
by XREAL_1:65;
then A56:
sqrt (((qz `2 ) ^2 ) + ((qz `1 ) ^2 )) <= sqrt ((((q `2 ) ^2 ) * 2) + (((q `1 ) ^2 ) * 2))
by A55, SQUARE_1:94;
A57:
((0. (TOP-REAL 2)) - qz) `2 =
((0. (TOP-REAL 2)) `2 ) - (qz `2 )
by TOPREAL3:8
.=
- (qz `2 )
by JGRAPH_2:11
;
((0. (TOP-REAL 2)) - qz) `1 =
((0. (TOP-REAL 2)) `1 ) - (qz `1 )
by TOPREAL3:8
.=
- (qz `1 )
by JGRAPH_2:11
;
then
sqrt (((((0. (TOP-REAL 2)) - qz) `2 ) ^2 ) + ((((0. (TOP-REAL 2)) - qz) `1 ) ^2 )) < r
by A26, A57, 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;
verum end;
end;
A58:
V1 is
open
by GOBOARD6:6;
sqrt 2
> 0
by SQUARE_1:93;
then
u0 in V1
by A17, GOBOARD6:4, XREAL_1:141;
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, A58, A19, XBOOLE_1:1;
verum
end;
A59:
D ` = {(0. (TOP-REAL 2))}
by Th30;
then
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (Sq_Circ " ) | D & h is continuous )
by Th51;
hence
ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = Sq_Circ " & h is continuous )
by A1, A59, A2, A14, Th13; verum