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 ) )

( ( 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

( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 implies f is_continuous_in x0 )
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 ) )

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 ) )

end;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

for r being Real st 0 < r holds
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

(f . x0) - (f . x) < r ) ) by A5; :: thesis: verum

end;( 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

hence
( 0 < s & ( for x being Real st x in dom f & |.(x - x0).| < s holds
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;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

(f . x0) - (f . x) < r ) ) by A5; :: thesis: verum

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

hence
( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 )
by A1, A4; :: thesis: verum
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

(f . x) - (f . x0) < r ) ) by A8; :: thesis: verum

end;( 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

hence
( 0 < s & ( for x being Real st x in dom f & |.(x - x0).| < s holds
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;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

(f . x) - (f . x0) < r ) ) by A8; :: thesis: verum

proof

hence
( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )
by A2; :: thesis: verum
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 ) )

end;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

hence
f is_continuous_in x0
by FCONT_1:3; :: thesis: verum
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

|.((f . x) - (f . x0)).| < r ) )

min (s1,s2) > 0 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;( 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

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

then |.((f . x) - (f . x0)).| <= r by A22, ABSVALUE:5;

hence |.((f . x) - (f . x0)).| < r by A23, XXREAL_0:1; :: thesis: verum

end;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

- ((f . x0) - (f . x)) > - r
by A21, XREAL_1:24;
assume A24:
|.((f . x) - (f . x0)).| = r
; :: thesis: contradiction

end;now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;

then |.((f . x) - (f . x0)).| <= r by A22, ABSVALUE:5;

hence |.((f . x) - (f . x0)).| < r by A23, XXREAL_0:1; :: thesis: verum

|.((f . x) - (f . x0)).| < r ) )

min (s1,s2) > 0 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