:: deftheorem defines is_lower_semicontinuous_in RFUNCT_4:def 7 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_lower_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 . x) - (f . x0) < r ) ) ) ) );