%0 Journal Article
%T Differentiable Functions into Real Normed Spaces
%A Hiroyuki Okazaki
%A Noboru Endou
%A Keiko Narita
%A Yasunari Shidama
%J Formalized Mathematics
%@ 1898-9934
%D 2011
%I 
%R 10.2478/v10037-011-0012-7
%X In this article, we formalize the differentiability of functions from the set of real numbers into a normed vector space [14].
%U http://versita.metapress.com/content/y101110q0l1r7165/?p=e63014958e714f888c6227088fa87423&pi=1