let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )
let x0 be Real; :: thesis: ( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )
thus ( f is_continuous_in x0 implies for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) :: thesis: ( ( for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) implies f is_continuous_in x0 )
proof
assume A1: f is_continuous_in x0 ; :: thesis: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1
let N1 be Neighbourhood of f . x0; :: thesis: ex N being Neighbourhood of x0 st f .: N c= N1
consider N being Neighbourhood of x0 such that
A2: for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1 by A1, Th4;
take N ; :: thesis: f .: N c= N1
now :: thesis: for r being Real st r in f .: N holds
r in N1
let r be Real; :: thesis: ( r in f .: N implies r in N1 )
assume r in f .: N ; :: thesis: r in N1
then ex x being Element of REAL st
( x in dom f & x in N & r = f . x ) by PARTFUN2:59;
hence r in N1 by A2; :: thesis: verum
end;
hence f .: N c= N1 ; :: thesis: verum
end;
assume A3: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 ; :: thesis: f is_continuous_in x0
now :: thesis: for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1
let N1 be Neighbourhood of f . x0; :: thesis: ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1
consider N being Neighbourhood of x0 such that
A4: f .: N c= N1 by A3;
take N = N; :: thesis: for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1
let x1 be Real; :: thesis: ( x1 in dom f & x1 in N implies f . x1 in N1 )
assume ( x1 in dom f & x1 in N ) ; :: thesis: f . x1 in N1
then f . x1 in f .: N by FUNCT_1:def 6;
hence f . x1 in N1 by A4; :: thesis: verum
end;
hence f is_continuous_in x0 by Th4; :: thesis: verum