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 Z: x0 in dom f ; :: thesis: ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )
A1: ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 implies f is_continuous_in x0 )

proof

assume A2: ( f is_upper_semicontinuous_in x0 & 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 A4: 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 ) )
A5: r is Real by XREAL_0:def 1;
then consider s1 being Real such that
A6: ( 0 < s1 & ( for x being Real st x in dom f & abs (x - x0) < s1 holds
(f . x) - (f . x0) < r ) ) by A2, A4, Def7;
consider s2 being Real such that
A7: ( 0 < s2 & ( for x being Real st x in dom f & abs (x - x0) < s2 holds
(f . x0) - (f . x) < r ) ) by A2, A4, A5, Def5;
set s = min s1,s2;
A8: 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 A6, XXREAL_0:def 9; :: thesis: verum

end;

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

hence min s1,s2 > 0 by A7, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

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

end;

A9: 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 A10: ( x in dom f & abs (x - x0) < min s1,s2 ) ; :: thesis: abs ((f . x) - (f . x0)) < r
A11: x is Real by XREAL_0:def 1;
( min s1,s2 <= s1 & min s1,s2 <= s2 ) by XXREAL_0:17;
then ( abs (x - x0) < s1 & abs (x - x0) < s2 ) by A10, XXREAL_0:2;
then A12: ( (f . x) - (f . x0) < r & (f . x0) - (f . x) < r ) by A6, A7, A10, A11;
then ( (f . x) - (f . x0) < r & - ((f . x0) - (f . x)) > - r ) by XREAL_1:26;
then A13: ( abs ((f . x) - (f . x0)) <= r & (f . x) - (f . x0) <> r & (f . x) - (f . x0) <> - r ) by ABSVALUE:12;
abs ((f . x) - (f . x0)) <> r

proof

assume A14: 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 A12, A14, 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 A12, A14; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence abs ((f . x) - (f . x0)) < r by A13, 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 ) )
thus ( 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 A8, A9; :: thesis: verum

end;

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

end;

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

proof

assume A15: f is_continuous_in x0 ; :: thesis: ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 )
A17: 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 A18: 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 ) )
consider s being real number such that
A19: ( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r ) ) by A15, A18, FCONT_1:3;
A20: 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 A21: ( x in dom f & abs (x - x0) < s ) ; :: thesis: (f . x) - (f . x0) < r
A22: abs ((f . x) - (f . x0)) < r by A19, A21;
(f . x) - (f . x0) <= abs ((f . x) - (f . x0)) by ABSVALUE:11;
hence (f . x) - (f . x0) < r by A22, XXREAL_0:2; :: thesis: verum

end;

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 ) )
thus ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) ) by A19, A20; :: 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 . 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 A23: 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 ) )
consider s being real number such that
A24: ( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r ) ) by A15, A23, FCONT_1:3;
A25: 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 A26: ( x in dom f & abs (x - x0) < s ) ; :: thesis: (f . x0) - (f . x) < r
A27: abs ((f . x) - (f . x0)) < r by A24, A26;
(f . x) - (f . x0) >= - (abs ((f . x) - (f . x0))) by ABSVALUE:11;
then - ((f . x) - (f . x0)) <= abs ((f . x) - (f . x0)) by XREAL_1:28;
hence (f . x0) - (f . x) < r by A27, XXREAL_0:2; :: thesis: verum

end;

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 ) )
thus ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) ) by A24, A25; :: thesis: verum

end;

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

end;

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