let x0 be Real; :: 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 & |.(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 & |.(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 & |.(x - x0).| < s holds
(f . x0) - (f . x) < r ) )
then consider s being Real such that
A5: 0 < s and
A6: for x being Real st x in dom f & |.(x - x0).| < s holds
|.((f . x) - (f . x0)).| < r by A3, FCONT_1:3;
take s ; :: thesis: ( 0 < s & ( for x being Real st x in dom f & |.(x - x0).| < s holds
(f . x0) - (f . x) < r ) )
for x being Real st x in dom f & |.(x - x0).| < s holds
(f . x0) - (f . x) < r

proof

let x be Real; :: thesis: ( x in dom f & |.(x - x0).| < s implies (f . x0) - (f . x) < r )
assume ( x in dom f & |.(x - x0).| < s ) ; :: thesis: (f . x0) - (f . x) < r
then A7: |.((f . x) - (f . x0)).| < r by A6;
(f . x) - (f . x0) >= - |.((f . x) - (f . x0)).| by ABSVALUE:4;
then - ((f . x) - (f . x0)) <= |.((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 & |.(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 & |.(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 & |.(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 & |.(x - x0).| < s holds
(f . x) - (f . x0) < r ) )
then consider s being Real such that
A8: 0 < s and
A9: for x being Real st x in dom f & |.(x - x0).| < s holds
|.((f . x) - (f . x0)).| < r by A3, FCONT_1:3;
take s ; :: thesis: ( 0 < s & ( for x being Real st x in dom f & |.(x - x0).| < s holds
(f . x) - (f . x0) < r ) )
for x being Real st x in dom f & |.(x - x0).| < s holds
(f . x) - (f . x0) < r

proof

let x be Real; :: thesis: ( x in dom f & |.(x - x0).| < s implies (f . x) - (f . x0) < r )
assume ( x in dom f & |.(x - x0).| < s ) ; :: thesis: (f . x) - (f . x0) < r
then A10: |.((f . x) - (f . x0)).| < r by A9;
(f . x) - (f . x0) <= |.((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 & |.(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; :: 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 st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(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 & |.(x - x0).| < s holds
|.((f . x) - (f . x0)).| < r ) ) )
assume A13: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - x0).| < s holds
|.((f . x) - (f . x0)).| < r ) )
consider s1 being Real such that
A14: 0 < s1 and
A15: for x being Real st x in dom f & |.(x - x0).| < s1 holds
(f . x) - (f . x0) < r by A12, A13;
consider s2 being Real such that
A16: 0 < s2 and
A17: for x being Real st x in dom f & |.(x - x0).| < s2 holds
(f . x0) - (f . x) < r by A11, A13;
set s = min (s1,s2);
A18: for x being Real st x in dom f & |.(x - x0).| < min (s1,s2) holds
|.((f . x) - (f . x0)).| < r

proof

let x be Real; :: thesis: ( x in dom f & |.(x - x0).| < min (s1,s2) implies |.((f . x) - (f . x0)).| < r )
assume that
A19: x in dom f and
A20: |.(x - x0).| < min (s1,s2) ; :: thesis: |.((f . x) - (f . x0)).| < r
min (s1,s2) <= s2 by XXREAL_0:17;
then |.(x - x0).| < s2 by A20, XXREAL_0:2;
then A21: (f . x0) - (f . x) < r by A17, A19;
min (s1,s2) <= s1 by XXREAL_0:17;
then |.(x - x0).| < s1 by A20, XXREAL_0:2;
then A22: (f . x) - (f . x0) < r by A15, A19;
A23: |.((f . x) - (f . x0)).| <> r

proof

assume A24: |.((f . x) - (f . x0)).| = r ; :: thesis: contradiction

now :: thesis: contradiction

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 A22, A24, ABSVALUE:def 1; :: thesis: verum

end;

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

then |.((f . x) - (f . x0)).| = - ((f . x) - (f . x0)) by ABSVALUE:def 1;
hence contradiction by A21, A24; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

end;

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

proof

now :: thesis: min (s1,s2) > 0

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

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

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

end;

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

hence min (s1,s2) > 0 by A16, 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 st x in dom f & |.(x - x0).| < min (s1,s2) holds
|.((f . x) - (f . x0)).| < r ) ) by A18; :: 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