let X be non empty TopSpace; :: thesis: for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X holds f1 . q <> 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 = 1 / r1 ) & g is continuous )
let f1 be Function of X,R^1; :: thesis: ( f1 is continuous & ( for q being Point of X holds f1 . q <> 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 = 1 / r1 ) & g is continuous ) )
assume that
A1: f1 is continuous and
A2: for q being Point of X holds f1 . q <> 0 ; :: 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 = 1 / r1 ) & g is continuous )
defpred S1[ set , set ] means for r1 being Real st f1 . $1 = r1 holds
$2 = 1 / r1;
A3: 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;
reconsider r3 = 1 / r1 as Element of REAL by XREAL_0:def 1;
take r3 ; :: thesis: S1[x,r3]
thus for r1 being Real st f1 . x = r1 holds
r3 = 1 / 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(A3);
 then consider f being Function of the carrier of X,REAL such that
A4: for x being Element of X
for r1 being Real st f1 . x = r1 holds
f . x = 1 / r1 ;
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; :: 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
A5: r0 > 0 and
A6: ].(r - r0),(r + r0).[ c= V by FRECHET:8;
A7: r = 1 / r1 by A4;
A8: r1 <> 0 by A2;
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 A9: r1 >= 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
set r4 = (r0 / r) / (r + r0);
reconsider G1 = ].(r1 - ((r0 / r) / (r + r0))),(r1 + ((r0 / r) / (r + r0))).[ as Subset of R^1 by TOPMETR:17;
r0 / r > 0 by A5, A8, A7, A9, XREAL_1:139;
then A10: r1 < r1 + ((r0 / r) / (r + r0)) by A5, A7, A9, XREAL_1:29, XREAL_1:139;
then r1 - ((r0 / r) / (r + r0)) < r1 by XREAL_1:19;
then A11: f1 . p in G1 by A10, XXREAL_1:4;
A12: r / (r + r0) > 0 by A5, A8, A7, A9, XREAL_1:139;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A13: ( p in W1 & W1 is open ) and
A14: f1 .: W1 c= G1 by A1, A11, Th10;
set W = W1;
r1 - ((r0 / r) / (r + r0)) = (1 / r) - ((r0 / (r + r0)) / r) by A7
.= (1 - (r0 / (r + r0))) / r
.= (((r + r0) / (r + r0)) - (r0 / (r + r0))) / r by A5, A7, A9, XCMPLX_1:60
.= (((r + r0) - r0) / (r + r0)) / r
.= (r / (r + r0)) / r ;
then A15: r1 - ((r0 / r) / (r + r0)) > 0 by A8, A7, A9, A12, XREAL_1:139;
g0 .: W1 c= ].(r - r0),(r + r0).[
proof
0 < r0 ^2 by A5, SQUARE_1:12;
then r0 * r < (r0 * r) + ((r0 * r0) + (r0 * r0)) by XREAL_1:29;
then (r0 * r) - ((r0 * r0) + (r0 * r0)) < r0 * r by XREAL_1:19;
then ((r0 * r) - ((r0 * r0) + (r0 * r0))) + (r * r) < (r * r) + (r0 * r) by XREAL_1:8;
then ((r - r0) * ((r + r0) + r0)) / ((r + r0) + r0) < (r * (r + r0)) / ((r + r0) + r0) by A5, A7, A9, XREAL_1:74;
then r - r0 < (r * (r + r0)) / ((r + r0) + r0) by A5, A7, A9, XCMPLX_1:89;
then r - r0 < r / (((r + r0) + r0) / (r + r0)) by XCMPLX_1:77;
then r - r0 < r / (((r + r0) / (r + r0)) + (r0 / (r + r0))) ;
then r - r0 < (r * 1) / (1 + (r0 / (r + r0))) by A5, A7, A9, XCMPLX_1:60;
then A16: r - r0 < 1 / ((1 + (r0 / (r + r0))) / r) by XCMPLX_1:77;
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
A17: z in dom g0 and
A18: z in W1 and
A19: g0 . z = x by FUNCT_1:def 6;
reconsider pz = z as Point of X by A17;
reconsider aa1 = f1 . pz as Real ;
A20: x = 1 / aa1 by A4, A19;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A21: f1 . pz in f1 .: W1 by A18, FUNCT_1:def 6;
then A22: r1 - ((r0 / r) / (r + r0)) < aa1 by A14, XXREAL_1:4;
then A23: 1 / aa1 < 1 / (r1 - ((r0 / r) / (r + r0))) by A15, XREAL_1:88;
aa1 < r1 + ((r0 / r) / (r + r0)) by A14, A21, XXREAL_1:4;
then 1 / ((1 / r) + ((r0 / r) / (r + r0))) < 1 / aa1 by A7, A15, A22, XREAL_1:76;
then A24: r - r0 < 1 / aa1 by A16, XXREAL_0:2;
1 / (r1 - ((r0 / r) / (r + r0))) = 1 / (r1 - ((r0 * (r ")) / (r + r0)))
.= 1 / (r1 - ((r0 * (1 / r)) / (r + r0)))
.= 1 / (r1 - (r0 / ((r + r0) / r1))) by A7, XCMPLX_1:77
.= 1 / ((r1 * 1) - (r1 * (r0 / (r + r0)))) by XCMPLX_1:81
.= 1 / ((1 - (r0 / (r + r0))) * r1)
.= 1 / ((((r + r0) / (r + r0)) - (r0 / (r + r0))) * r1) by A5, A7, A9, XCMPLX_1:60
.= 1 / ((((r + r0) - r0) / (r + r0)) * r1)
.= 1 / (r / ((r + r0) / r1)) by XCMPLX_1:81
.= 1 / ((r * r1) / (r + r0)) by XCMPLX_1:77
.= ((r + r0) / (r * r1)) * 1 by XCMPLX_1:80
.= (r + r0) / 1 by A8, A7, XCMPLX_0:def 7
.= r + r0 ;
hence x in ].(r - r0),(r + r0).[ by A20, A24, 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 A6, A13, XBOOLE_1:1; :: thesis: verum
end;
case A25: r1 < 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
set r4 = (r0 / (- r)) / ((- r) + r0);
reconsider G1 = ].(r1 - ((r0 / (- r)) / ((- r) + r0))),(r1 + ((r0 / (- r)) / ((- r) + r0))).[ as Subset of R^1 by TOPMETR:17;
A26: G1 is open by JORDAN6:35;
A27: 0 < - r by A7, A25, XREAL_1:58;
then (- r) / ((- r) + r0) > 0 by A5, XREAL_1:139;
then - (r / ((- r) + r0)) > 0 ;
then A28: r / ((- r) + r0) < 0 ;
r0 / (- r) > 0 by A5, A27, XREAL_1:139;
then A29: r1 < r1 + ((r0 / (- r)) / ((- r) + r0)) by A5, A7, A25, XREAL_1:29, XREAL_1:139;
then r1 - ((r0 / (- r)) / ((- r) + r0)) < r1 by XREAL_1:19;
then f1 . p in G1 by A29, XXREAL_1:4;
then consider W1 being Subset of X such that
A30: ( p in W1 & W1 is open ) and
A31: f1 .: W1 c= G1 by A1, A26, Th10;
set W = W1;
r1 * ((- r) * (1 / (- r))) = r1 * 1 by A27, XCMPLX_1:87;
then (- (r * r1)) * (1 / (- r)) = r1 ;
then A32: (- 1) * (1 / (- r)) = r1 by A2, A7, XCMPLX_1:87;
then r1 + ((r0 / (- r)) / ((- r) + r0)) = (- (1 / (- r))) + ((r0 / ((- r) + r0)) / (- r))
.= ((- 1) / (- r)) + ((r0 / ((- r) + r0)) / (- r))
.= ((- 1) + (r0 / ((- r) + r0))) / (- r)
.= ((- (((- r) + r0) / ((- r) + r0))) + (r0 / ((- r) + r0))) / (- r) by A5, A7, A25, XCMPLX_1:60
.= (((- ((- r) + r0)) / ((- r) + r0)) + (r0 / ((- r) + r0))) / (- r)
.= (((r - r0) + r0) / ((- r) + r0)) / (- r)
.= (r / ((- r) + r0)) / (- r) ;
then A33: r1 + ((r0 / (- r)) / ((- r) + r0)) < 0 by A27, A28, XREAL_1:141;
g0 .: W1 c= ].(r - r0),(r + r0).[
proof
0 < r0 ^2 by A5, SQUARE_1:12;
then r0 * (- r) < (r0 * (- r)) + ((r0 * r0) + (r0 * r0)) by XREAL_1:29;
then (r0 * (- r)) - ((r0 * r0) + (r0 * r0)) < r0 * (- r) by XREAL_1:19;
then ((r0 * (- r)) - ((r0 * r0) + (r0 * r0))) + ((- r) * (- r)) < (r0 * (- r)) + ((- r) * (- r)) by XREAL_1:8;
then (((- r) - r0) * (((- r) + r0) + r0)) / (((- r) + r0) + r0) < ((- r) * ((- r) + r0)) / (((- r) + r0) + r0) by A5, A7, A25, XREAL_1:74;
then (- r) - r0 < ((- r) * ((- r) + r0)) / (((- r) + r0) + r0) by A5, A7, A25, XCMPLX_1:89;
then (- r) - r0 < (- r) / ((((- r) + r0) + r0) / ((- r) + r0)) by XCMPLX_1:77;
then (- r) - r0 < (- r) / ((((- r) + r0) / ((- r) + r0)) + (r0 / ((- r) + r0))) ;
then (- r) - r0 < ((- r) * 1) / (1 + (r0 / ((- r) + r0))) by A5, A7, A25, XCMPLX_1:60;
then (- r) - r0 < 1 / ((1 + (r0 / ((- r) + r0))) / (- r)) by XCMPLX_1:77;
then - (r + r0) < 1 / ((1 / (- r)) + ((r0 / (- r)) / ((- r) + r0))) ;
then r + r0 > - (1 / ((1 / (- r)) + ((r0 / (- r)) / ((- r) + r0)))) by XREAL_1:25;
then A34: r + r0 > 1 / (- ((1 / (- r)) + ((r0 / (- r)) / ((- r) + r0)))) by XCMPLX_1:188;
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
A35: z in dom g0 and
A36: z in W1 and
A37: g0 . z = x by FUNCT_1:def 6;
reconsider pz = z as Point of X by A35;
reconsider aa1 = f1 . pz as Real ;
A38: x = 1 / aa1 by A4, A37;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A39: f1 . pz in f1 .: W1 by A36, FUNCT_1:def 6;
then A40: aa1 < r1 + ((r0 / (- r)) / ((- r) + r0)) by A31, XXREAL_1:4;
then A41: 1 / aa1 > 1 / (r1 + ((r0 / (- r)) / ((- r) + r0))) by A33, XREAL_1:87;
r1 - ((r0 / (- r)) / ((- r) + r0)) < aa1 by A31, A39, XXREAL_1:4;
then 1 / ((- (1 / (- r))) - ((r0 / (- r)) / ((- r) + r0))) > 1 / aa1 by A32, A33, A40, XREAL_1:99;
then A42: r + r0 > 1 / aa1 by A34, XXREAL_0:2;
1 / (r1 + ((r0 / (- r)) / ((- r) + r0))) = 1 / (r1 + ((r0 * ((- r) ")) / ((- r) + r0)))
.= 1 / (r1 + ((r0 * (1 / (- r))) / ((- r) + r0)))
.= 1 / (r1 + ((- (r1 * r0)) / ((- r) + r0))) by A32
.= 1 / (r1 + (- ((r1 * r0) / ((- r) + r0))))
.= 1 / (r1 - ((r1 * r0) / ((- r) + r0)))
.= 1 / (r1 - (r0 / (((- r) + r0) / r1))) by XCMPLX_1:77
.= 1 / ((r1 * 1) - (r1 * (r0 / ((- r) + r0)))) by XCMPLX_1:81
.= 1 / (r1 * (1 - (r0 / ((- r) + r0))))
.= 1 / (((((- r) + r0) / ((- r) + r0)) - (r0 / ((- r) + r0))) * r1) by A5, A7, A25, XCMPLX_1:60
.= 1 / (((((- r) + r0) - r0) / (- (r - r0))) * r1)
.= 1 / ((- ((((- r) + r0) - r0) / (r - r0))) * r1) by XCMPLX_1:188
.= 1 / (((((- r) + r0) - r0) / (r - r0)) * (- r1))
.= 1 / ((- r) / ((r - r0) / (- r1))) by XCMPLX_1:81
.= 1 / (((- r) * (- r1)) / (r - r0)) by XCMPLX_1:77
.= ((r - r0) / ((- r) * (- r1))) * 1 by XCMPLX_1:80
.= (r - r0) / ((- r) * ((- r) ")) by A32
.= (r - r0) / 1 by A27, XCMPLX_0:def 7
.= r - r0 ;
hence x in ].(r - r0),(r + r0).[ by A38, A42, A41, 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, A30, 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 A43: g0 is continuous by Th10;
for p being Point of X
for r1 being Real st f1 . p = r1 holds
g0 . p = 1 / r1 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 = 1 / r1 ) & g is continuous ) by A43; :: thesis: verum