Portal de Periódicos da CAPES

Isomorphisms from the Space of Multilinear Operators

2019; De Gruyter Open; Volume: 27; Issue: 2 Linguagem: Inglês

10.2478/forma-2019-0011

1898-9934

Kazuhisa Nakasho,

Security and Verification in Computing

Summary 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.