let x0 be real number ; :: thesis: for f being PartFunc of REAL,REAL st x0 in dom f holds
( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )
let f be PartFunc of REAL,REAL; :: thesis: ( x0 in dom f implies ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) )
assume A1: x0 in dom f ; :: thesis: ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )
A2: ( f is_continuous_in x0 implies ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) )

proof

assume A3: f is_continuous_in x0 ; :: thesis: ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 )
A4: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) )
then consider s being real number such that
A5: 0 < s and
A6: for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r by A3, FCONT_1:3;
take s ; :: thesis: ( s is Real & 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) )
thus s is Real by XREAL_0:def 1; :: thesis: ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) )
for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r

proof

let x be Real; :: thesis: ( x in dom f & abs (x - x0) < s implies (f . x0) - (f . x) < r )
assume ( x in dom f & abs (x - x0) < s ) ; :: thesis: (f . x0) - (f . x) < r
then A7: abs ((f . x) - (f . x0)) < r by A6;
(f . x) - (f . x0) >= - (abs ((f . x) - (f . x0))) by ABSVALUE:4;
then - ((f . x) - (f . x0)) <= abs ((f . x) - (f . x0)) by XREAL_1:26;
hence (f . x0) - (f . x) < r by A7, XXREAL_0:2; :: thesis: verum

end;

hence ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) ) by A5; :: thesis: verum

end;

for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) )
then consider s being real number such that
A8: 0 < s and
A9: for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r by A3, FCONT_1:3;
take s ; :: thesis: ( s is Real & 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) )
thus s is Real by XREAL_0:def 1; :: thesis: ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) )
for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r

proof

let x be Real; :: thesis: ( x in dom f & abs (x - x0) < s implies (f . x) - (f . x0) < r )
assume ( x in dom f & abs (x - x0) < s ) ; :: thesis: (f . x) - (f . x0) < r
then A10: abs ((f . x) - (f . x0)) < r by A9;
(f . x) - (f . x0) <= abs ((f . x) - (f . x0)) by ABSVALUE:4;
hence (f . x) - (f . x0) < r by A10, XXREAL_0:2; :: thesis: verum

end;

hence ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) ) by A8; :: thesis: verum

end;

hence ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) by A1, A4, Def5, Def7; :: thesis: verum

end;

( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 implies f is_continuous_in x0 )

proof

assume that
A11: f is_upper_semicontinuous_in x0 and
A12: f is_lower_semicontinuous_in x0 ; :: thesis: f is_continuous_in x0
for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r ) )

proof

let r be real number ; :: thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r ) ) )
assume A13: 0 < r ; :: thesis: ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r ) )
A14: r is Real by XREAL_0:def 1;
then consider s1 being Real such that
A15: 0 < s1 and
A16: for x being Real st x in dom f & abs (x - x0) < s1 holds
(f . x) - (f . x0) < r by A12, A13, Def7;
consider s2 being Real such that
A17: 0 < s2 and
A18: for x being Real st x in dom f & abs (x - x0) < s2 holds
(f . x0) - (f . x) < r by A11, A13, A14, Def5;
set s = min (s1,s2);
A19: for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds
abs ((f . x) - (f . x0)) < r

proof

let x be real number ; :: thesis: ( x in dom f & abs (x - x0) < min (s1,s2) implies abs ((f . x) - (f . x0)) < r )
assume that
A20: x in dom f and
A21: abs (x - x0) < min (s1,s2) ; :: thesis: abs ((f . x) - (f . x0)) < r
A22: x is Real by XREAL_0:def 1;
min (s1,s2) <= s2 by XXREAL_0:17;
then abs (x - x0) < s2 by A21, XXREAL_0:2;
then A23: (f . x0) - (f . x) < r by A18, A20, A22;
min (s1,s2) <= s1 by XXREAL_0:17;
then abs (x - x0) < s1 by A21, XXREAL_0:2;
then A24: (f . x) - (f . x0) < r by A16, A20, A22;
A25: abs ((f . x) - (f . x0)) <> r

proof

assume A26: abs ((f . x) - (f . x0)) = r ; :: thesis: contradiction

now

per cases ( (f . x) - (f . x0) >= 0 or not (f . x) - (f . x0) >= 0 ) ;

suppose (f . x) - (f . x0) >= 0 ; :: thesis: contradiction

hence contradiction by A24, A26, ABSVALUE:def 1; :: thesis: verum

end;

suppose not (f . x) - (f . x0) >= 0 ; :: thesis: contradiction

then abs ((f . x) - (f . x0)) = - ((f . x) - (f . x0)) by ABSVALUE:def 1;
hence contradiction by A23, A26; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

- ((f . x0) - (f . x)) > - r by A23, XREAL_1:24;
then abs ((f . x) - (f . x0)) <= r by A24, ABSVALUE:5;
hence abs ((f . x) - (f . x0)) < r by A25, XXREAL_0:1; :: thesis: verum

end;

take min (s1,s2) ; :: thesis: ( 0 < min (s1,s2) & ( for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds
abs ((f . x) - (f . x0)) < r ) )
min (s1,s2) > 0

proof

now

per cases ( s1 <= s2 or not s1 <= s2 ) ;

suppose s1 <= s2 ; :: thesis: min (s1,s2) > 0

hence min (s1,s2) > 0 by A15, XXREAL_0:def 9; :: thesis: verum

end;

suppose not s1 <= s2 ; :: thesis: min (s1,s2) > 0

hence min (s1,s2) > 0 by A17, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

hence min (s1,s2) > 0 ; :: thesis: verum

end;

hence ( 0 < min (s1,s2) & ( for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds
abs ((f . x) - (f . x0)) < r ) ) by A19; :: thesis: verum

end;

hence f is_continuous_in x0 by FCONT_1:3; :: thesis: verum

end;

hence ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) by A2; :: thesis: verum