:: deftheorem defines is_continuously_differentiable_up_to_order CKSPACE1:def 1 :
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for k being Nat
for Z being set holds
( f is_continuously_differentiable_up_to_order k,Z iff ( Z c= dom f & f is_partial_differentiable_up_to_order k,Z & ( for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds
f `partial| (Z,I) is_continuous_on Z ) ) );