Isometric differentiable functions on real normed space

DOI10.2478/forma-2013-0027zbMath1298.58010MaRDI QIDQ467801

Yuichi Futa, Yasunari Shidama, Noboru Endou

Publication date: 5 November 2014

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2013-0027

zbMATH Keywords

isometric differentiable function

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

58C20: Differentiation theory (Gateaux, Fréchet, etc.) on manifolds

46G05: Derivatives of functions in infinite-dimensional spaces