Differentiable Functions into Real Normed Spaces
Hiroyuki Okazaki, Noboru Endou, Keiko Narita, Yasunari Shidama (2011)
Formalized Mathematics
Similarity:
In this article, we formalize the differentiability of functions from the set of real numbers into a normed vector space [14].