reconsider f = Sq_Circ " as Function of (TOP-REAL 2),(TOP-REAL 2) by Th29;
reconsider D = NonZero (TOP-REAL 2) as non empty Subset of (TOP-REAL 2) by JGRAPH_2:9;
A1:
f . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2)
by Th28;
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: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 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:30;
then consider r being
Real such that A17:
r > 0
and A18:
Ball (
u0,
r)
c= V
by A1, A15, TOPMETR:15;
reconsider r =
r as
Real ;
reconsider W1 =
Ball (
u0,
r),
V1 =
Ball (
u0,
(r / (sqrt 2))) as
Subset of
(TOP-REAL 2) by EUCLID:67;
A19:
f .: V1 c= W1
proof
let z be
object ;
TARSKI:def 3 ( not z in f .: V1 or z in W1 )
A20:
sqrt 2
> 0
by SQUARE_1:25;
assume
z in f .: V1
;
z in W1
then consider y being
object such that A21:
y in dom f
and A22:
y in V1
and A23:
z = f . y
by FUNCT_1:def 6;
z in rng f
by A21, A23, FUNCT_1:def 3;
then reconsider qz =
z as
Point of
(TOP-REAL 2) ;
reconsider pz =
qz as
Point of
(Euclid 2) by EUCLID:67;
reconsider q =
y as
Point of
(TOP-REAL 2) by A21;
reconsider qy =
q as
Point of
(Euclid 2) by EUCLID:67;
A24:
(q `1) ^2 >= 0
by XREAL_1:63;
A25:
(q `2) ^2 >= 0
by XREAL_1:63;
dist (
u0,
qy)
< r / (sqrt 2)
by A22, METRIC_1:11;
then
|.((0. (TOP-REAL 2)) - q).| < r / (sqrt 2)
by JGRAPH_1:28;
then
sqrt (((((0. (TOP-REAL 2)) - q) `1) ^2) + ((((0. (TOP-REAL 2)) - q) `2) ^2)) < r / (sqrt 2)
by JGRAPH_1:30;
then
sqrt (((((0. (TOP-REAL 2)) `1) - (q `1)) ^2) + ((((0. (TOP-REAL 2)) - q) `2) ^2)) < r / (sqrt 2)
by TOPREAL3:3;
then
sqrt (((((0. (TOP-REAL 2)) `1) - (q `1)) ^2) + ((((0. (TOP-REAL 2)) `2) - (q `2)) ^2)) < r / (sqrt 2)
by TOPREAL3:3;
then
(sqrt (((q `1) ^2) + ((q `2) ^2))) * (sqrt 2) < (r / (sqrt 2)) * (sqrt 2)
by A20, JGRAPH_2:3, XREAL_1:68;
then
sqrt ((((q `1) ^2) + ((q `2) ^2)) * 2) < (r / (sqrt 2)) * (sqrt 2)
by A24, A25, SQUARE_1:29;
then A26:
sqrt ((((q `1) ^2) + ((q `2) ^2)) * 2) < r
by A20, XCMPLX_1:87;
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, Th28;
then
qz `1 = (q `1) * (sqrt (1 + (((q `2) / (q `1)) ^2)))
by A23, EUCLID:52;
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:52;
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:72;
then
((q `2) / (q `1)) ^2 <= ((q `1) ^2) / ((q `1) ^2)
by XCMPLX_1:76;
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:7;
then
((q `2) ^2) * (1 + (((q `2) / (q `1)) ^2)) <= ((q `2) ^2) * 2
by A25, XREAL_1:64;
then A39:
(qz `2) ^2 <= ((q `2) ^2) * 2
by A33, A32, SQUARE_1:def 2;
((q `1) ^2) * (1 + (((q `2) / (q `1)) ^2)) <= ((q `1) ^2) * 2
by A24, A38, XREAL_1:64;
then
(qz `1) ^2 <= ((q `1) ^2) * 2
by A33, A31, SQUARE_1:def 2;
then A40:
((qz `1) ^2) + ((qz `2) ^2) <= (((q `1) ^2) * 2) + (((q `2) ^2) * 2)
by A39, XREAL_1:7;
(
(qz `1) ^2 >= 0 &
(qz `2) ^2 >= 0 )
by XREAL_1:63;
then A41:
sqrt (((qz `1) ^2) + ((qz `2) ^2)) <= sqrt ((((q `1) ^2) * 2) + (((q `2) ^2) * 2))
by A40, SQUARE_1:26;
A42:
((0. (TOP-REAL 2)) - qz) `2 =
((0. (TOP-REAL 2)) `2) - (qz `2)
by TOPREAL3:3
.=
- (qz `2)
by JGRAPH_2:3
;
((0. (TOP-REAL 2)) - qz) `1 =
((0. (TOP-REAL 2)) `1) - (qz `1)
by TOPREAL3:3
.=
- (qz `1)
by JGRAPH_2:3
;
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:30;
then
dist (
u0,
pz)
< r
by JGRAPH_1:28;
hence
z in W1
by METRIC_1:11;
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:72;
then
((q `1) / (q `2)) ^2 <= ((q `2) ^2) / ((q `2) ^2)
by XCMPLX_1:76;
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:7;
then A50:
((q `2) ^2) * (1 + (((q `1) / (q `2)) ^2)) <= ((q `2) ^2) * 2
by A25, XREAL_1:64;
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 2;
A52:
((q `1) ^2) * (1 + (((q `1) / (q `2)) ^2)) <= ((q `1) ^2) * 2
by A24, A49, XREAL_1:64;
A53:
(Sq_Circ ") . q = |[((q `1) * (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) * (sqrt (1 + (((q `1) / (q `2)) ^2))))]|
by A43, Th28;
then
qz `1 = (q `1) * (sqrt (1 + (((q `1) / (q `2)) ^2)))
by A23, EUCLID:52;
then A54:
(qz `1) ^2 <= ((q `1) ^2) * 2
by A52, A51, SQUARE_1:9;
qz `2 = (q `2) * (sqrt (1 + (((q `1) / (q `2)) ^2)))
by A23, A53, EUCLID:52;
then
(qz `2) ^2 <= ((q `2) ^2) * 2
by A50, A51, SQUARE_1:9;
then A55:
((qz `2) ^2) + ((qz `1) ^2) <= (((q `2) ^2) * 2) + (((q `1) ^2) * 2)
by A54, XREAL_1:7;
(
(qz `2) ^2 >= 0 &
(qz `1) ^2 >= 0 )
by XREAL_1:63;
then A56:
sqrt (((qz `2) ^2) + ((qz `1) ^2)) <= sqrt ((((q `2) ^2) * 2) + (((q `1) ^2) * 2))
by A55, SQUARE_1:26;
A57:
((0. (TOP-REAL 2)) - qz) `2 =
((0. (TOP-REAL 2)) `2) - (qz `2)
by TOPREAL3:3
.=
- (qz `2)
by JGRAPH_2:3
;
((0. (TOP-REAL 2)) - qz) `1 =
((0. (TOP-REAL 2)) `1) - (qz `1)
by TOPREAL3:3
.=
- (qz `1)
by JGRAPH_2:3
;
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:30;
then
dist (
u0,
pz)
< r
by JGRAPH_1:28;
hence
z in W1
by METRIC_1:11;
verum end; end;
end;
A58:
V1 is
open
by GOBOARD6:3;
sqrt 2
> 0
by SQUARE_1:25;
then
u0 in V1
by A17, GOBOARD6:1, XREAL_1:139;
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 Th20;
then
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (Sq_Circ ") | D & h is continuous )
by Th41;
hence
ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = Sq_Circ " & h is continuous )
by A1, A59, A2, A14, Th3; verum