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 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 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]
proof
let x be Element of X; :: thesis: ex y being Element of REAL st S1[x,y]
reconsider r1 = f1 . x as Element of REAL by TOPMETR:17;
set r3 = r1 * r1;
for r1 being Real st f1 . x = r1 holds
r1 * r1 = r1 * r1 ;
hence ex y being Element of REAL st
for r1 being Real 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(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 ; :: thesis: 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; :: 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 ) )
reconsider r = g0 . p as Real ;
reconsider r1 = f1 . p as Real ;
assume ( 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 )
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 :: thesis: ( ( 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 ; :: thesis: 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 ; :: 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 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;
A23: now :: thesis: ( ( 0 <= r1 - ((sqrt (r + r0)) - (sqrt r)) & r - r0 < aa1 * aa1 ) or ( 0 > r1 - ((sqrt (r + r0)) - (sqrt r)) & r - r0 < aa1 * aa1 ) )
per cases ( 0 <= r1 - ((sqrt (r + r0)) - (sqrt r)) or 0 > r1 - ((sqrt (r + r0)) - (sqrt r)) ) ;
case A24: 0 <= r1 - ((sqrt (r + r0)) - (sqrt r)) ; :: thesis: r - r0 < aa1 * aa1
A25: (((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:7;
(r1 - ((sqrt (r + r0)) - (sqrt r))) ^2 < aa1 ^2 by A22, A24, SQUARE_1:16;
then (((r1 - ((sqrt (r + r0)) - (sqrt r))) ^2) - (2 * (((sqrt (r + r0)) - (sqrt r)) ^2))) - (aa1 ^2) < 0 by A25, XREAL_1:49;
hence r - r0 < aa1 * aa1 by A7, A16, A17, XREAL_1:48; :: 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:48;
then r1 ^2 < ((sqrt (r + r0)) - (sqrt r)) ^2 by A10, SQUARE_1:16;
then (r1 ^2) - (((sqrt (r + r0)) - (sqrt r)) ^2) < 0 by XREAL_1:49;
then ((r1 ^2) - (((sqrt (r + r0)) - (sqrt r)) ^2)) - ((2 * r1) * ((sqrt (r + r0)) - (sqrt r))) < 0 - 0 by A10, A12;
hence r - r0 < aa1 * aa1 by A7, A16, A17; :: thesis: verum
end;
end;
end;
(- 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; :: thesis: 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; :: thesis: verum
end;
case A28: r1 < 0 ; :: thesis: 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 ; :: 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 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;
A43: now :: thesis: ( ( 0 >= r1 + ((sqrt (r + r0)) - (sqrt r)) & r - r0 < aa1 * aa1 ) or ( 0 < r1 + ((sqrt (r + r0)) - (sqrt r)) & r - r0 < aa1 * aa1 ) )
per cases ( 0 >= r1 + ((sqrt (r + r0)) - (sqrt r)) or 0 < r1 + ((sqrt (r + r0)) - (sqrt r)) ) ;
case A44: 0 >= r1 + ((sqrt (r + r0)) - (sqrt r)) ; :: thesis: r - r0 < aa1 * aa1
A45: (((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:7;
- aa1 > - (r1 + ((sqrt (r + r0)) - (sqrt r))) by A42, XREAL_1:24;
then (- (r1 + ((sqrt (r + r0)) - (sqrt r)))) ^2 < (- aa1) ^2 by A44, SQUARE_1:16;
then (((r1 + ((sqrt (r + r0)) - (sqrt r))) ^2) - (2 * (((sqrt (r + r0)) - (sqrt r)) ^2))) - (aa1 ^2) < 0 by A45, XREAL_1:49;
hence r - r0 < aa1 * aa1 by A7, A37, XREAL_1:48; :: 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:8;
then (- r1) ^2 < ((sqrt (r + r0)) - (sqrt r)) ^2 by A28, SQUARE_1:16;
then (r1 ^2) - (r1 ^2) > (r1 ^2) - (((sqrt (r + r0)) - (sqrt r)) ^2) by XREAL_1:15;
then ((r1 ^2) - (((sqrt (r + r0)) - (sqrt r)) ^2)) + ((2 * r1) * ((sqrt (r + r0)) - (sqrt r))) < 0 + 0 by A28, A30;
hence r - r0 < aa1 * aa1 by A7, A35, A36; :: thesis: verum
end;
end;
end;
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; :: thesis: 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; :: 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 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; :: thesis: verum