Isometric differentiable functions on real normed space

DOI10.2478/FORMA-2013-0027zbMath1298.58010OpenAlexW1998357482MaRDI QIDQ467801

Noboru Endou, Yuichi Futa, Yasunari Shidama

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

Mechanization of proofs and logical operations (03B35) Differentiation theory (Gateaux, Fréchet, etc.) on manifolds (58C20) Derivatives of functions in infinite-dimensional spaces (46G05)

Related Items (2)

Isomorphism between spaces of multilinear maps and nested compositions over real normed vector spaces ⋮ Isomorphisms from the space of multilinear operators

Cites Work

• Cartesian Products of Family of Real Linear Spaces
• Differentiable Functions on Normed Linear Spaces
• Unnamed Item

This page was built for publication: Isometric differentiable functions on real normed space