Isomorphism between spaces of multilinear maps and nested compositions over real normed vector spaces

DOI10.2478/FORMA-2022-0006MaRDI QIDQ6489402zbMATH OpenFDO

Authors Kazuhisa Nakasho, Yuichi Futa

Publication date 22 April 2024

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

zbMATH Keywords

Banach spacecomposition functionmultilinear function

Mathematics Subject Classification ID

Multilinear algebra, tensor calculus (15A69) Forms (bilinear, sesquilinear, multilinear) (47A07) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Isomorphisms from the space of multilinear operators
• Continuity of multilinear operator on normed linear spaces
• Isomorphisms between spaces of multilinear mappings or homogeneous polynomials
• Differentiable functions on normed linear spaces

Cites work

• scientific article; zbMATH DE number 3678487 (Why is no real title available?)
• scientific article; zbMATH DE number 1199721 (Why is no real title available?)
• Continuity of barycentric coordinates in Euclidean topological spaces
• Isometric differentiable functions on real normed space
• Mizar: state-of-the-art and beyond
• Multilinear operator and its basic properties
• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(1)

• Formalized functional analysis with semilinear maps

This page was built for publication: Isomorphism between spaces of multilinear maps and nested compositions over real normed vector spaces

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6489402)