Isomorphisms from the Space of Multilinear Operators

摘要

In this article, using the Mizar system [5], [2], the isomorphisms from the space of multilinear operators are discussed. In the first chapter, two isomorphisms are formalized. The former isomorphism shows the correspondence between the space of multilinear operators and the space of bilinear operators. The latter shows the correspondence between the space of multilinear operators and the space of the composition of linear operators. In the last chapter, the above isomorphisms are extended to isometric mappings between the normed spaces. We referred to [6], [11], [9], [3], [10] in this formalization.