:: deftheorem defines is_differentiable_on_interval FDIFF_12:def 1 :
for f being PartFunc of REAL,REAL
for I being non empty Interval holds
( f is_differentiable_on_interval I iff ( I c= dom f & inf I < sup I & ( inf I in I implies f is_right_differentiable_in lower_bound I ) & ( sup I in I implies f is_left_differentiable_in upper_bound I ) & f is_differentiable_on ].(inf I),(sup I).[ ) );