:: deftheorem defines is_upper_semicontinuous_in RFUNCT_4:def 5 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_upper_semicontinuous_in x0 iff ( x0 in dom f & ( 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 ) ) ) ) );