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 number 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 number st f1 . p = r1 holds
g . p = 1 / r1 ) & g is continuous ) )
assume A1: ( f1 is continuous & ( 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 number 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;
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 = 1 / r1;
for r1 being Real st f1 . x = r1 holds
1 / r1 = 1 / r1 ;
hence ex y being Element of REAL st
for r1 being Real st f1 . x = r1 holds
y = 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(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 st f1 . x = r1 holds
f . x = 1 / 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 = 1 / r1
proof
let p be Point of X; :: thesis: for r1 being real number st f1 . p = r1 holds
g0 . p = 1 / r1
let r1 be real number ; :: thesis: ( f1 . p = r1 implies g0 . p = 1 / r1 )
assume A5: f1 . p = r1 ; :: thesis: g0 . p = 1 / r1
reconsider r1 = r1 as Element of REAL by XREAL_0:def 1;
g0 . p = 1 / r1 by A3, A5;
hence g0 . p = 1 / r1 ; :: thesis: verum
end;
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 A6: ( 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
A7: ( r0 > 0 & ].(r - r0),(r + r0).[ c= V ) by A6, FRECHET:8;
reconsider r1 = f1 . p as Real by TOPMETR:24;
A8: r1 <> 0 by A1;
A9: r = 1 / r1 by A3;
then A10: r = r1 " ;
now
per cases ( r1 >= 0 or r1 < 0 ) ;
case A11: r1 >= 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
then A12: 0 < r by A8, A10;
A16: 1 * (1 / r) = r1 by A9;
set r4 = (r0 / r) / (r + r0);
A17: r0 / r > 0 by A7, A12, XREAL_1:141;
A19: (r0 / r) / (r + r0) > 0 by A11, A17, A7, A9, XREAL_1:141;
A20: r1 - ((r0 / r) / (r + r0)) = (1 / r) - ((r0 / (r + r0)) / r) by A16
.= (1 - (r0 / (r + r0))) / r
.= (((r + r0) / (r + r0)) - (r0 / (r + r0))) / r by A11, A7, A9, XCMPLX_1:60
.= (((r + r0) - r0) / (r + r0)) / r
.= (r / (r + r0)) / r ;
r / (r + r0) > 0 by A12, A7, XREAL_1:141;
then A21: r1 - ((r0 / r) / (r + r0)) > 0 by A12, A20, XREAL_1:141;
reconsider G1 = ].(r1 - ((r0 / r) / (r + r0))),(r1 + ((r0 / r) / (r + r0))).[ as Subset of R^1 by TOPMETR:24;
A22: r1 < r1 + ((r0 / r) / (r + r0)) by A19, XREAL_1:31;
then r1 - ((r0 / r) / (r + r0)) < r1 by XREAL_1:21;
then A23: f1 . p in G1 by A22, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A24: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A23, 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
A25: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A25;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A26: f1 . pz in f1 .: W1 by A25, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A27: x = 1 / aa1 by A3, A25;
A28: ( r1 - ((r0 / r) / (r + r0)) < aa1 & aa1 < r1 + ((r0 / r) / (r + r0)) ) by A24, A26, XXREAL_1:4;
then A29: 1 / ((1 / r) + ((r0 / r) / (r + r0))) < 1 / aa1 by A16, A21, XREAL_1:78;
A30: 0 < r0 ^2 by A7, SQUARE_1:74;
r0 * r < (r0 * r) + ((r0 * r0) + (r0 * r0)) by A30, XREAL_1:31;
then (r0 * r) - ((r0 * r0) + (r0 * r0)) < r0 * r by XREAL_1:21;
then ((r0 * r) - ((r0 * r0) + (r0 * r0))) + (r * r) < (r * r) + (r0 * r) by XREAL_1:10;
then ((r - r0) * ((r + r0) + r0)) / ((r + r0) + r0) < (r * (r + r0)) / ((r + r0) + r0) by A11, A7, A9, XREAL_1:76;
then r - r0 < (r * (r + r0)) / ((r + r0) + r0) by A9, A11, A7, XCMPLX_1:90;
then r - r0 < r / (((r + r0) + r0) / (r + r0)) by XCMPLX_1:78;
then r - r0 < r / (((r + r0) / (r + r0)) + (r0 / (r + r0))) ;
then r - r0 < (r * 1) / (1 + (r0 / (r + r0))) by A11, A7, A9, XCMPLX_1:60;
then r - r0 < 1 / ((1 + (r0 / (r + r0))) / r) by XCMPLX_1:78;
then r - r0 < 1 / ((1 / r) + ((r0 / (r + r0)) / r)) ;
then r - r0 < 1 / ((1 / r) + ((r0 / r) / (r + r0))) ;
then A31: r - r0 < 1 / aa1 by A29, XXREAL_0:2;
A32: 1 / aa1 < 1 / (r1 - ((r0 / r) / (r + r0))) by A21, A28, XREAL_1:90;
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 A16, XCMPLX_1:78
.= 1 / ((r1 * 1) - (r1 * (r0 / (r + r0)))) by XCMPLX_1:82
.= 1 / ((1 - (r0 / (r + r0))) * r1)
.= 1 / ((((r + r0) / (r + r0)) - (r0 / (r + r0))) * r1) by A11, A7, A9, XCMPLX_1:60
.= 1 / ((((r + r0) - r0) / (r + r0)) * r1)
.= 1 / (r / ((r + r0) / r1)) by XCMPLX_1:82
.= 1 / ((r * r1) / (r + r0)) by XCMPLX_1:78
.= ((r + r0) / (r * r1)) * 1 by XCMPLX_1:81
.= (r + r0) / 1 by A8, A10, XCMPLX_0:def 7
.= r + r0 ;
hence x in ].(r - r0),(r + r0).[ by A27, A31, A32, 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 A7, A24, XBOOLE_1:1; :: thesis: verum
end;
case S: r1 < 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
then A33: r1 " < 0 ;
then A34: 0 < - r by A10, XREAL_1:60;
r1 * ((- r) * (1 / (- r))) = r1 * 1 by A34, XCMPLX_1:88;
then (- (r * r1)) * (1 / (- r)) = r1 ;
then A38: (- 1) * (1 / (- r)) = r1 by A1, A9, XCMPLX_1:88;
set r4 = (r0 / (- r)) / ((- r) + r0);
A39: r0 / (- r) > 0 by A7, A34, XREAL_1:141;
A41: (r0 / (- r)) / ((- r) + r0) > 0 by S, A39, A7, A9, XREAL_1:141;
A42: r1 + ((r0 / (- r)) / ((- r) + r0)) = (- (1 / (- r))) + ((r0 / ((- r) + r0)) / (- r)) by A38
.= ((- 1) / (- r)) + ((r0 / ((- r) + r0)) / (- r))
.= ((- 1) + (r0 / ((- r) + r0))) / (- r)
.= ((- (((- r) + r0) / ((- r) + r0))) + (r0 / ((- r) + r0))) / (- r) by A9, A7, S, XCMPLX_1:60
.= (((- ((- r) + r0)) / ((- r) + r0)) + (r0 / ((- r) + r0))) / (- r)
.= (((r - r0) + r0) / ((- r) + r0)) / (- r)
.= (r / ((- r) + r0)) / (- r) ;
(- r) / ((- r) + r0) > 0 by A34, A7, XREAL_1:141;
then - (r / ((- r) + r0)) > 0 ;
then r / ((- r) + r0) < 0 ;
then A43: r1 + ((r0 / (- r)) / ((- r) + r0)) < 0 by A34, A42, XREAL_1:143;
reconsider G1 = ].(r1 - ((r0 / (- r)) / ((- r) + r0))),(r1 + ((r0 / (- r)) / ((- r) + r0))).[ as Subset of R^1 by TOPMETR:24;
A44: r1 < r1 + ((r0 / (- r)) / ((- r) + r0)) by A41, XREAL_1:31;
then r1 - ((r0 / (- r)) / ((- r) + r0)) < r1 by XREAL_1:21;
then A45: f1 . p in G1 by A44, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A46: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A45, 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
A47: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A47;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A48: f1 . pz in f1 .: W1 by A47, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A49: x = 1 / aa1 by A3, A47;
A50: ( r1 - ((r0 / (- r)) / ((- r) + r0)) < aa1 & aa1 < r1 + ((r0 / (- r)) / ((- r) + r0)) ) by A46, A48, XXREAL_1:4;
then A51: 1 / ((- (1 / (- r))) - ((r0 / (- r)) / ((- r) + r0))) > 1 / aa1 by A38, A43, XREAL_1:101;
A52: 0 < r0 ^2 by A7, SQUARE_1:74;
r0 * (- r) < (r0 * (- r)) + ((r0 * r0) + (r0 * r0)) by A52, XREAL_1:31;
then (r0 * (- r)) - ((r0 * r0) + (r0 * r0)) < r0 * (- r) by XREAL_1:21;
then ((r0 * (- r)) - ((r0 * r0) + (r0 * r0))) + ((- r) * (- r)) < (r0 * (- r)) + ((- r) * (- r)) by XREAL_1:10;
then (((- r) - r0) * (((- r) + r0) + r0)) / (((- r) + r0) + r0) < ((- r) * ((- r) + r0)) / (((- r) + r0) + r0) by S, A7, A10, XREAL_1:76;
then (- r) - r0 < ((- r) * ((- r) + r0)) / (((- r) + r0) + r0) by A9, S, A7, XCMPLX_1:90;
then (- r) - r0 < (- r) / ((((- r) + r0) + r0) / ((- r) + r0)) by XCMPLX_1:78;
then (- r) - r0 < (- r) / ((((- r) + r0) / ((- r) + r0)) + (r0 / ((- r) + r0))) ;
then (- r) - r0 < ((- r) * 1) / (1 + (r0 / ((- r) + r0))) by A33, A7, A10, XCMPLX_1:60;
then (- r) - r0 < 1 / ((1 + (r0 / ((- r) + r0))) / (- r)) by XCMPLX_1:78;
then (- r) - r0 < 1 / ((1 / (- r)) + ((r0 / ((- r) + r0)) / (- r))) ;
then - (r + r0) < 1 / ((1 / (- r)) + ((r0 / (- r)) / ((- r) + r0))) ;
then r + r0 > - (1 / ((1 / (- r)) + ((r0 / (- r)) / ((- r) + r0)))) by XREAL_1:27;
then r + r0 > 1 / (- ((1 / (- r)) + ((r0 / (- r)) / ((- r) + r0)))) by XCMPLX_1:189;
then A53: r + r0 > 1 / aa1 by A51, XXREAL_0:2;
A54: 1 / aa1 > 1 / (r1 + ((r0 / (- r)) / ((- r) + r0))) by A43, A50, XREAL_1:89;
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 A38
.= 1 / (r1 + (- ((r1 * r0) / ((- r) + r0))))
.= 1 / (r1 - ((r1 * r0) / ((- r) + r0)))
.= 1 / (r1 - (r0 / (((- r) + r0) / r1))) by XCMPLX_1:78
.= 1 / ((r1 * 1) - (r1 * (r0 / ((- r) + r0)))) by XCMPLX_1:82
.= 1 / (r1 * (1 - (r0 / ((- r) + r0))))
.= 1 / (((((- r) + r0) / ((- r) + r0)) - (r0 / ((- r) + r0))) * r1) by A33, A7, A10, XCMPLX_1:60
.= 1 / (((((- r) + r0) - r0) / (- (r - r0))) * r1)
.= 1 / ((- ((((- r) + r0) - r0) / (r - r0))) * r1) by XCMPLX_1:189
.= 1 / (((((- r) + r0) - r0) / (r - r0)) * (- r1))
.= 1 / ((- r) / ((r - r0) / (- r1))) by XCMPLX_1:82
.= 1 / (((- r) * (- r1)) / (r - r0)) by XCMPLX_1:78
.= ((r - r0) / ((- r) * (- r1))) * 1 by XCMPLX_1:81
.= (r - r0) / ((- r) * ((- r) " )) by A38
.= (r - r0) / 1 by A34, XCMPLX_0:def 7
.= r - r0 ;
hence x in ].(r - r0),(r + r0).[ by A49, A53, A54, 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 A7, A46, 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 = 1 / r1 ) & g is continuous ) by A4; :: thesis: verum