let X be set ; :: thesis: for f being PartFunc of REAL,REAL st X c= dom f holds
( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )
let f be PartFunc of REAL,REAL; :: thesis: ( X c= dom f implies ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) )
assume A1: X c= dom f ; :: thesis: ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )
A2: ( f | X is continuous implies ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) )
proof
assume A3: f | X is continuous ; :: thesis: ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X )
A4: for x0 being Real st x0 in X holds
f | X is_lower_semicontinuous_in x0
proof
let x0 be Real; :: thesis: ( x0 in X implies f | X is_lower_semicontinuous_in x0 )
assume x0 in X ; :: thesis: f | X is_lower_semicontinuous_in x0
then A5: x0 in dom (f | X) by A1, RELAT_1:57;
then f | X is_continuous_in x0 by A3, FCONT_1:def 2;
hence f | X is_lower_semicontinuous_in x0 by A5, Th21; :: thesis: verum
end;
for x0 being Real st x0 in X holds
f | X is_upper_semicontinuous_in x0
proof
let x0 be Real; :: thesis: ( x0 in X implies f | X is_upper_semicontinuous_in x0 )
assume x0 in X ; :: thesis: f | X is_upper_semicontinuous_in x0
then A6: x0 in dom (f | X) by A1, RELAT_1:57;
then f | X is_continuous_in x0 by A3, FCONT_1:def 2;
hence f | X is_upper_semicontinuous_in x0 by A6, Th21; :: thesis: verum
end;
hence ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) by A1, A4; :: thesis: verum
end;
( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X implies f | X is continuous )
proof
assume that
A7: f is_upper_semicontinuous_on X and
A8: f is_lower_semicontinuous_on X ; :: thesis: f | X is continuous
( X c= dom f & ( for x0 being Real st x0 in dom (f | X) holds
f | X is_continuous_in x0 ) )
proof
thus X c= dom f by A7; :: thesis: for x0 being Real st x0 in dom (f | X) holds
f | X is_continuous_in x0
let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A9: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
x0 in X by A9, RELAT_1:57;
then ( f | X is_upper_semicontinuous_in x0 & f | X is_lower_semicontinuous_in x0 ) by A7, A8;
hence f | X is_continuous_in x0 by Th21; :: thesis: verum
end;
hence f | X is continuous by FCONT_1:def 2; :: thesis: verum
end;
hence ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) by A2; :: thesis: verum