let X be non empty TopSpace; for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X ex r being Real st
( f1 . q = r & r >= 0 ) ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous )
let f1 be Function of X,R^1; ( f1 is continuous & ( for q being Point of X ex r being Real st
( f1 . q = r & r >= 0 ) ) implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous ) )
assume that
A1:
f1 is continuous
and
A2:
for q being Point of X ex r being Real st
( f1 . q = r & r >= 0 )
; ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous )
defpred S1[ set , set ] means for r11 being Real st f1 . $1 = r11 holds
$2 = sqrt r11;
A3:
for x being Element of X ex y being Element of REAL st S1[x,y]
ex f being Function of the carrier of X,REAL st
for x2 being Element of X holds S1[x2,f . x2]
from FUNCT_2:sch 3(A3);
then consider f being Function of the carrier of X,REAL such that
A4:
for x2 being Element of X
for r11 being Real st f1 . x2 = r11 holds
f . x2 = sqrt r11
;
reconsider g0 = f as Function of X,R^1 by TOPMETR:17;
for p being Point of X
for V being Subset of R^1 st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
proof
let p be
Point of
X;
for V being Subset of R^1 st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )let V be
Subset of
R^1;
( g0 . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) )
reconsider r =
g0 . p as
Real ;
reconsider r1 =
f1 . p as
Real ;
assume
(
g0 . p in V &
V is
open )
;
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
then consider r01 being
Real such that A5:
r01 > 0
and A6:
].(r - r01),(r + r01).[ c= V
by FRECHET:8;
set r0 =
min (
r01,1);
A7:
min (
r01,1)
> 0
by A5, XXREAL_0:21;
A8:
min (
r01,1)
> 0
by A5, XXREAL_0:21;
min (
r01,1)
<= r01
by XXREAL_0:17;
then
(
r - r01 <= r - (min (r01,1)) &
r + (min (r01,1)) <= r + r01 )
by XREAL_1:6, XREAL_1:10;
then
].(r - (min (r01,1))),(r + (min (r01,1))).[ c= ].(r - r01),(r + r01).[
by XXREAL_1:46;
then A9:
].(r - (min (r01,1))),(r + (min (r01,1))).[ c= V
by A6;
A10:
ex
r8 being
Real st
(
f1 . p = r8 &
r8 >= 0 )
by A2;
A11:
r = sqrt r1
by A4;
then A12:
r1 = r ^2
by A10, SQUARE_1:def 2;
A13:
r >= 0
by A10, A11, SQUARE_1:17, SQUARE_1:26;
then A14:
((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2) > 0 + 0
by A8, SQUARE_1:12, XREAL_1:8;
per cases
( r - (min (r01,1)) > 0 or r - (min (r01,1)) <= 0 )
;
suppose A15:
r - (min (r01,1)) > 0
;
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )set r4 =
(min (r01,1)) * (r - (min (r01,1)));
reconsider G1 =
].(r1 - ((min (r01,1)) * (r - (min (r01,1))))),(r1 + ((min (r01,1)) * (r - (min (r01,1))))).[ as
Subset of
R^1 by TOPMETR:17;
A16:
r1 < r1 + ((min (r01,1)) * (r - (min (r01,1))))
by A8, A15, XREAL_1:29, XREAL_1:129;
then
r1 - ((min (r01,1)) * (r - (min (r01,1)))) < r1
by XREAL_1:19;
then A17:
f1 . p in G1
by A16, XXREAL_1:4;
G1 is
open
by JORDAN6:35;
then consider W1 being
Subset of
X such that A18:
(
p in W1 &
W1 is
open )
and A19:
f1 .: W1 c= G1
by A1, A17, JGRAPH_2:10;
set W =
W1;
A20:
(
(r - ((1 / 2) * (min (r01,1)))) ^2 >= 0 &
(min (r01,1)) ^2 >= 0 )
by XREAL_1:63;
then
0 < r
by A10, A11, SQUARE_1:25;
then A21:
(min (r01,1)) * r > 0
by A8, XREAL_1:129;
then
0 + (r * (min (r01,1))) < (r * (min (r01,1))) + (r * (min (r01,1)))
by XREAL_1:8;
then
((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1))) < ((2 * r) * (min (r01,1))) - ((min (r01,1)) * (min (r01,1)))
by XREAL_1:14;
then
- ((min (r01,1)) * (r - (min (r01,1)))) > - (((2 * r) * (min (r01,1))) - ((min (r01,1)) ^2))
by XREAL_1:24;
then
r1 + (- ((min (r01,1)) * (r - (min (r01,1))))) > (r ^2) + (- (((2 * r) * (min (r01,1))) - ((min (r01,1)) ^2)))
by A12, XREAL_1:8;
then
sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) > sqrt ((r - (min (r01,1))) ^2)
by SQUARE_1:27, XREAL_1:63;
then A22:
sqrt (r1 - ((min (r01,1)) * (r - (min (r01,1))))) > r - (min (r01,1))
by A15, SQUARE_1:22;
0 + (r * (min (r01,1))) < (r * (min (r01,1))) + (r * (min (r01,1)))
by A21, XREAL_1:8;
then
((min (r01,1)) * r) + 0 < ((2 * r) * (min (r01,1))) + (2 * ((min (r01,1)) * (min (r01,1))))
by A8, XREAL_1:8;
then
(((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1)))) + ((min (r01,1)) * (min (r01,1))) < (((2 * r) * (min (r01,1))) + ((min (r01,1)) * (min (r01,1)))) + ((min (r01,1)) * (min (r01,1)))
;
then
((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1))) < ((2 * r) * (min (r01,1))) + ((min (r01,1)) * (min (r01,1)))
by XREAL_1:7;
then
r1 + ((min (r01,1)) * (r - (min (r01,1)))) < (r ^2) + (((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2))
by A12, XREAL_1:8;
then
sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1))))) < sqrt ((r + (min (r01,1))) ^2)
by A10, A8, A15, SQUARE_1:27;
then A23:
r + (min (r01,1)) > sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1)))))
by A13, A7, SQUARE_1:22;
A24:
r1 - ((min (r01,1)) * (r - (min (r01,1)))) =
(r ^2) - (((min (r01,1)) * r) - ((min (r01,1)) * (min (r01,1))))
by A10, A11, SQUARE_1:def 2
.=
((r - ((1 / 2) * (min (r01,1)))) ^2) + ((3 / 4) * ((min (r01,1)) ^2))
;
g0 .: W1 c= ].(r - (min (r01,1))),(r + (min (r01,1))).[
proof
let x be
object ;
TARSKI:def 3 ( not x in g0 .: W1 or x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ )
assume
x in g0 .: W1
;
x in ].(r - (min (r01,1))),(r + (min (r01,1))).[
then consider z being
object such that A25:
z in dom g0
and A26:
z in W1
and A27:
g0 . z = x
by FUNCT_1:def 6;
reconsider pz =
z as
Point of
X by A25;
reconsider aa1 =
f1 . pz as
Real ;
A28:
ex
r9 being
Real st
(
f1 . pz = r9 &
r9 >= 0 )
by A2;
pz in the
carrier of
X
;
then
pz in dom f1
by FUNCT_2:def 1;
then A29:
f1 . pz in f1 .: W1
by A26, FUNCT_1:def 6;
then
aa1 < r1 + ((min (r01,1)) * (r - (min (r01,1))))
by A19, XXREAL_1:4;
then
sqrt aa1 < sqrt (r1 + ((min (r01,1)) * (r - (min (r01,1)))))
by A28, SQUARE_1:27;
then A30:
sqrt aa1 < r + (min (r01,1))
by A23, XXREAL_0:2;
A31:
r1 - ((min (r01,1)) * (r - (min (r01,1)))) < aa1
by A19, A29, XXREAL_1:4;
x = sqrt aa1
by A4, A27;
hence
x in ].(r - (min (r01,1))),(r + (min (r01,1))).[
by A30, A32, XXREAL_1:4;
verum
end; hence
ex
W being
Subset of
X st
(
p in W &
W is
open &
g0 .: W c= V )
by A9, A18, XBOOLE_1:1;
verum end; suppose A33:
r - (min (r01,1)) <= 0
;
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )set r4 =
(((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3;
reconsider G1 =
].(r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)),(r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)).[ as
Subset of
R^1 by TOPMETR:17;
(((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3
> 0
by A14, XREAL_1:139;
then A34:
r1 < r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)
by XREAL_1:29;
then
r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < r1
by XREAL_1:19;
then A35:
f1 . p in G1
by A34, XXREAL_1:4;
G1 is
open
by JORDAN6:35;
then consider W1 being
Subset of
X such that A36:
(
p in W1 &
W1 is
open )
and A37:
f1 .: W1 c= G1
by A1, A35, JGRAPH_2:10;
set W =
W1;
(((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3
< ((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)
by A14, XREAL_1:221;
then
r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < (r ^2) + (((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2))
by A12, XREAL_1:8;
then
sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)) <= sqrt ((r + (min (r01,1))) ^2)
by A10, A13, A8, SQUARE_1:26;
then A38:
r + (min (r01,1)) >= sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3))
by A13, A7, SQUARE_1:22;
g0 .: W1 c= ].(r - (min (r01,1))),(r + (min (r01,1))).[
proof
let x be
object ;
TARSKI:def 3 ( not x in g0 .: W1 or x in ].(r - (min (r01,1))),(r + (min (r01,1))).[ )
assume
x in g0 .: W1
;
x in ].(r - (min (r01,1))),(r + (min (r01,1))).[
then consider z being
object such that A39:
z in dom g0
and A40:
z in W1
and A41:
g0 . z = x
by FUNCT_1:def 6;
reconsider pz =
z as
Point of
X by A39;
reconsider aa1 =
f1 . pz as
Real ;
A42:
ex
r9 being
Real st
(
f1 . pz = r9 &
r9 >= 0 )
by A2;
pz in the
carrier of
X
;
then
pz in dom f1
by FUNCT_2:def 1;
then A43:
f1 . pz in f1 .: W1
by A40, FUNCT_1:def 6;
then
aa1 < r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3)
by A37, XXREAL_1:4;
then
sqrt aa1 < sqrt (r1 + ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3))
by A42, SQUARE_1:27;
then A44:
sqrt aa1 < r + (min (r01,1))
by A38, XXREAL_0:2;
A45:
r1 - ((((2 * r) * (min (r01,1))) + ((min (r01,1)) ^2)) / 3) < aa1
by A37, A43, XXREAL_1:4;
x = sqrt aa1
by A4, A41;
hence
x in ].(r - (min (r01,1))),(r + (min (r01,1))).[
by A44, A46, XXREAL_1:4;
verum
end; hence
ex
W being
Subset of
X st
(
p in W &
W is
open &
g0 .: W c= V )
by A9, A36, XBOOLE_1:1;
verum end; end;
end;
then A47:
g0 is continuous
by JGRAPH_2:10;
for p being Point of X
for r11 being Real st f1 . p = r11 holds
g0 . p = sqrt r11
by A4;
hence
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous )
by A47; verum