:: deftheorem defines is_Lcontinuous_in FDIFF_3:def 1 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_Lcontinuous_in x0 iff ( x0 in dom f & ( for a being Real_Sequence st rng a c= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds
( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );