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