Isometric Differentiable Functions on Real Normed Space
Yuichi Futa, Noboru Endou, Yasunari Shidama (2013)
Formalized Mathematics
Similarity:
In this article, we formalize isometric differentiable functions on real normed space [17], and their properties.