:: deftheorem defines is_differentiable_in NDIFF_3:def 3 :
for F being RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being Real holds
( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) );