let X be non empty TopSpace; :: thesis: 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 number st f1 . p = r1 holds
g . p = r1 * r1 ) & g is continuous )
let f1 be Function of X,R^1 ; :: thesis: ( f1 is continuous implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = r1 * r1 ) & g is continuous ) )
assume A1: f1 is continuous ; :: thesis: ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = r1 * r1 ) & g is continuous )
defpred S1[ set , set ] means for r1 being real number st f1 . $1 = r1 holds
$2 = r1 * r1;
A2: for x being Element of X ex y being Element of REAL st S1[x,y]
proof
let x be Element of X; :: thesis: ex y being Element of REAL st S1[x,y]
reconsider r1 = f1 . x as Real by TOPMETR:24;
set r3 = r1 * r1;
for r1 being real number st f1 . x = r1 holds
r1 * r1 = r1 * r1 ;
hence ex y being Element of REAL st
for r1 being real number st f1 . x = r1 holds
y = r1 * r1 ; :: thesis: verum
end;
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(A2);
 then consider f being Function of the carrier of X, REAL such that
A3: for x being Element of X
for r1 being real number st f1 . x = r1 holds
f . x = r1 * r1 ;
reconsider g0 = f as Function of X,R^1 by TOPMETR:24;
A4: for p being Point of X
for r1 being real number st f1 . p = r1 holds
g0 . p = r1 * r1 by A3;
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; :: thesis: 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 ; :: thesis: ( 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 ) )
assume A5: ( g0 . p in V & V is open ) ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
reconsider r = g0 . p as Real by TOPMETR:24;
consider r0 being Real such that
A6: ( r0 > 0 & ].(r - r0),(r + r0).[ c= V ) by A5, FRECHET:8;
reconsider r1 = f1 . p as Real by TOPMETR:24;
A7: r = r1 * r1 by A3;
A8: r = r1 ^2 by A3;
A9: 0 <= r by A7, XREAL_1:65;
A11: (sqrt (r + r0)) ^2 = r + r0 by A9, A6, SQUARE_1:def 4;
now
per cases ( r1 >= 0 or r1 < 0 ) ;
case A12: r1 >= 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
then A13: r1 = sqrt r by A8, SQUARE_1:def 4;
set r4 = (sqrt (r + r0)) - (sqrt r);
r + r0 > r by A6, XREAL_1:31;
then sqrt (r + r0) > sqrt r by A7, SQUARE_1:95, XREAL_1:65;
then A14: (sqrt (r + r0)) - (sqrt r) > 0 by XREAL_1:52;
A15: ((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 A9, A6, SQUARE_1:def 4
.= (r + (r0 - ((2 * (sqrt (r + r0))) * (sqrt r)))) + r by A9, SQUARE_1:def 4
.= ((2 * r) + r0) - ((2 * (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:24;
A16: r1 < r1 + ((sqrt (r + r0)) - (sqrt r)) by A14, XREAL_1:31;
then r1 - ((sqrt (r + r0)) - (sqrt r)) < r1 by XREAL_1:21;
then A17: f1 . p in G1 by A16, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A18: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A17, Th20;
set W = W1;
g0 .: W1 c= ].(r - r0),(r + r0).[
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: W1 or x in ].(r - r0),(r + r0).[ )
assume x in g0 .: W1 ; :: thesis: x in ].(r - r0),(r + r0).[
then consider z being set such that
A19: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A19;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A20: f1 . pz in f1 .: W1 by A19, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A21: x = aa1 * aa1 by A3, A19;
A22: ( r1 - ((sqrt (r + r0)) - (sqrt r)) < aa1 & aa1 < r1 + ((sqrt (r + r0)) - (sqrt r)) ) by A18, A20, XXREAL_1:4;
(- r1) - ((sqrt (r + r0)) - (sqrt r)) <= r1 - ((sqrt (r + r0)) - (sqrt r)) by A12, XREAL_1:11;
then - (r1 + ((sqrt (r + r0)) - (sqrt r))) < aa1 by A22, XXREAL_0:2;
then A23: aa1 - (- (r1 + ((sqrt (r + r0)) - (sqrt r)))) > 0 by XREAL_1:52;
(r1 + ((sqrt (r + r0)) - (sqrt r))) - aa1 > 0 by A22, XREAL_1:52;
then ((r1 + ((sqrt (r + r0)) - (sqrt r))) - aa1) * ((r1 + ((sqrt (r + r0)) - (sqrt r))) + aa1) > 0 by A23, XREAL_1:131;
then ((r1 + ((sqrt (r + r0)) - (sqrt r))) ^2 ) - (aa1 ^2 ) > 0 ;
then A24: aa1 ^2 < (r1 + ((sqrt (r + r0)) - (sqrt r))) ^2 by XREAL_1:49;
now
per cases ( 0 <= r1 - ((sqrt (r + r0)) - (sqrt r)) or 0 > r1 - ((sqrt (r + r0)) - (sqrt r)) ) ;
case 0 <= r1 - ((sqrt (r + r0)) - (sqrt r)) ; :: thesis: r - r0 < aa1 * aa1
then A25: (r1 - ((sqrt (r + r0)) - (sqrt r))) ^2 < aa1 ^2 by A22, SQUARE_1:78;
(- 2) * (((sqrt (r + r0)) - (sqrt r)) ^2 ) <= 0 by XREAL_1:65, XREAL_1:133;
then (((r1 - ((sqrt (r + r0)) - (sqrt r))) ^2 ) - (aa1 ^2 )) + (- (2 * (((sqrt (r + r0)) - (sqrt r)) ^2 ))) <= (((r1 - ((sqrt (r + r0)) - (sqrt r))) ^2 ) - (aa1 ^2 )) + 0 by XREAL_1:9;
then (((r1 - ((sqrt (r + r0)) - (sqrt r))) ^2 ) - (2 * (((sqrt (r + r0)) - (sqrt r)) ^2 ))) - (aa1 ^2 ) < 0 by A25, XREAL_1:51;
hence r - r0 < aa1 * aa1 by A7, A13, A15, XREAL_1:50; :: thesis: verum
end;
case 0 > r1 - ((sqrt (r + r0)) - (sqrt r)) ; :: thesis: r - r0 < aa1 * aa1
then r1 < (sqrt (r + r0)) - (sqrt r) by XREAL_1:50;
then r1 ^2 < ((sqrt (r + r0)) - (sqrt r)) ^2 by A12, SQUARE_1:78;
then A26: (r1 ^2 ) - (((sqrt (r + r0)) - (sqrt r)) ^2 ) < 0 by XREAL_1:51;
((r1 ^2 ) - (((sqrt (r + r0)) - (sqrt r)) ^2 )) - ((2 * r1) * ((sqrt (r + r0)) - (sqrt r))) < 0 - 0 by A26, A14, A12;
hence r - r0 < aa1 * aa1 by A7, A13, A15, XREAL_1:65; :: thesis: verum
end;
end;
end;
hence x in ].(r - r0),(r + r0).[ by A7, A13, A15, A21, A24, XXREAL_1:4; :: thesis: verum
end;
hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by A6, A18, XBOOLE_1:1; :: thesis: verum
end;
case A27: r1 < 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
A29: (- r1) ^2 = r1 ^2 ;
then A30: - r1 = sqrt r by A7, A27, SQUARE_1:89;
set r4 = (sqrt (r + r0)) - (sqrt r);
r + r0 > r by A6, XREAL_1:31;
then sqrt (r + r0) > sqrt r by A7, SQUARE_1:95, XREAL_1:65;
then A31: (sqrt (r + r0)) - (sqrt r) > 0 by XREAL_1:52;
A32: ((sqrt (r + r0)) - (sqrt r)) ^2 = ((r + r0) - ((2 * (sqrt (r + r0))) * (sqrt r))) + ((sqrt r) ^2 ) by A11
.= (r + (r0 - ((2 * (sqrt (r + r0))) * (sqrt r)))) + r by A7, A27, A29, SQUARE_1:89
.= ((2 * r) + r0) - ((2 * (sqrt (r + r0))) * (sqrt r)) ;
then A33: (- ((2 * r1) * ((sqrt (r + r0)) - (sqrt r)))) + (((sqrt (r + r0)) - (sqrt r)) ^2 ) = r0 by A7, A30;
reconsider G1 = ].(r1 - ((sqrt (r + r0)) - (sqrt r))),(r1 + ((sqrt (r + r0)) - (sqrt r))).[ as Subset of R^1 by TOPMETR:24;
A34: r1 < r1 + ((sqrt (r + r0)) - (sqrt r)) by A31, XREAL_1:31;
then r1 - ((sqrt (r + r0)) - (sqrt r)) < r1 by XREAL_1:21;
then A35: f1 . p in G1 by A34, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A36: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A35, Th20;
set W = W1;
g0 .: W1 c= ].(r - r0),(r + r0).[
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: W1 or x in ].(r - r0),(r + r0).[ )
assume x in g0 .: W1 ; :: thesis: x in ].(r - r0),(r + r0).[
then consider z being set such that
A37: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A37;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A38: f1 . pz in f1 .: W1 by A37, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A39: x = aa1 * aa1 by A3, A37;
A40: ( r1 - ((sqrt (r + r0)) - (sqrt r)) < aa1 & aa1 < r1 + ((sqrt (r + r0)) - (sqrt r)) ) by A36, A38, XXREAL_1:4;
(- r1) - ((sqrt (r + r0)) - (sqrt r)) >= r1 - ((sqrt (r + r0)) - (sqrt r)) by A27, XREAL_1:11;
then - ((- r1) - ((sqrt (r + r0)) - (sqrt r))) <= - (r1 - ((sqrt (r + r0)) - (sqrt r))) by XREAL_1:26;
then - (r1 - ((sqrt (r + r0)) - (sqrt r))) > aa1 by A40, XXREAL_0:2;
then A41: (- (r1 - ((sqrt (r + r0)) - (sqrt r)))) + (r1 - ((sqrt (r + r0)) - (sqrt r))) > aa1 + (r1 - ((sqrt (r + r0)) - (sqrt r))) by XREAL_1:10;
aa1 - (r1 - ((sqrt (r + r0)) - (sqrt r))) > 0 by A40, XREAL_1:52;
then - ((- aa1) + (r1 - ((sqrt (r + r0)) - (sqrt r)))) > 0 ;
then (r1 - ((sqrt (r + r0)) - (sqrt r))) + (- aa1) < 0 ;
then ((r1 - ((sqrt (r + r0)) - (sqrt r))) - aa1) * ((r1 - ((sqrt (r + r0)) - (sqrt r))) + aa1) > 0 by A41, XREAL_1:132;
then ((r1 - ((sqrt (r + r0)) - (sqrt r))) ^2 ) - (aa1 ^2 ) > 0 ;
then A42: aa1 ^2 < (r1 - ((sqrt (r + r0)) - (sqrt r))) ^2 by XREAL_1:49;
now
per cases ( 0 >= r1 + ((sqrt (r + r0)) - (sqrt r)) or 0 < r1 + ((sqrt (r + r0)) - (sqrt r)) ) ;
case S: 0 >= r1 + ((sqrt (r + r0)) - (sqrt r)) ; :: thesis: r - r0 < aa1 * aa1
- aa1 > - (r1 + ((sqrt (r + r0)) - (sqrt r))) by A40, XREAL_1:26;
then A44: (- (r1 + ((sqrt (r + r0)) - (sqrt r)))) ^2 < (- aa1) ^2 by S, SQUARE_1:78;
(- 2) * (((sqrt (r + r0)) - (sqrt r)) ^2 ) <= 0 by XREAL_1:65, XREAL_1:133;
then (((r1 + ((sqrt (r + r0)) - (sqrt r))) ^2 ) - (aa1 ^2 )) + (- (2 * (((sqrt (r + r0)) - (sqrt r)) ^2 ))) <= (((r1 + ((sqrt (r + r0)) - (sqrt r))) ^2 ) - (aa1 ^2 )) + 0 by XREAL_1:9;
then (((r1 + ((sqrt (r + r0)) - (sqrt r))) ^2 ) - (2 * (((sqrt (r + r0)) - (sqrt r)) ^2 ))) - (aa1 ^2 ) < 0 by A44, XREAL_1:51;
hence r - r0 < aa1 * aa1 by A7, A33, XREAL_1:50; :: thesis: verum
end;
case 0 < r1 + ((sqrt (r + r0)) - (sqrt r)) ; :: thesis: r - r0 < aa1 * aa1
then 0 + (- r1) < (r1 + ((sqrt (r + r0)) - (sqrt r))) + (- r1) by XREAL_1:10;
then (- r1) ^2 < ((sqrt (r + r0)) - (sqrt r)) ^2 by A27, SQUARE_1:78;
then A45: (r1 ^2 ) - (r1 ^2 ) > (r1 ^2 ) - (((sqrt (r + r0)) - (sqrt r)) ^2 ) by XREAL_1:17;
((r1 ^2 ) - (((sqrt (r + r0)) - (sqrt r)) ^2 )) + ((2 * r1) * ((sqrt (r + r0)) - (sqrt r))) < 0 + 0 by A45, A31, A27;
hence r - r0 < aa1 * aa1 by A7, A30, A32, XREAL_1:65; :: thesis: verum
end;
end;
end;
hence x in ].(r - r0),(r + r0).[ by A7, A33, A39, A42, XXREAL_1:4; :: thesis: verum
end;
hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by A6, A36, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) ; :: thesis: verum
end;
then g0 is continuous by Th20;
hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = r1 * r1 ) & g is continuous ) by A4; :: thesis: verum