:: deftheorem defines Ck_Functions CKSPACE1:def 2 :
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m) holds Ck_Functions (k,X) = { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ;